mathlib3 documentation

logic.is_empty

Types that are empty #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define a typeclass is_empty, which expresses that a type has no elements.

Main declaration #

source
@[class]
structure is_empty (α : Sort u_4) :
Prop

is_empty α expresses that α is empty.

Instances of this typeclass
source
@[protected, instance]
def empty.is_empty  :
is_empty empty
source
@[protected, instance]
def pempty.is_empty  :
is_empty pempty
source
@[protected, instance]
def false.is_empty  :
is_empty false
source
@[protected, instance]
def fin.is_empty  :
is_empty (fin 0)
source
@[protected]
theorem function.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty β] (f : α → β) :
is_empty α
source
@[protected, instance]
def pi.is_empty {α : Sort u_1} {p : α → Sort u_2} [h : nonempty α] [∀ (x : α), is_empty (p x)] :
is_empty (Π (x : α), p x)
source
@[protected, instance]
def pprod.is_empty_left {α : Sort u_1} {β : Sort u_2} [is_empty α] :
is_empty (pprod α β)
source
@[protected, instance]
def pprod.is_empty_right {α : Sort u_1} {β : Sort u_2} [is_empty β] :
is_empty (pprod α β)
source
@[protected, instance]
def prod.is_empty_left {α : Type u_1} {β : Type u_2} [is_empty α] :
is_empty (α × β)
source
@[protected, instance]
def prod.is_empty_right {α : Type u_1} {β : Type u_2} [is_empty β] :
is_empty (α × β)
source
@[protected, instance]
def psum.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty α] [is_empty β] :
is_empty (psum α β)
source
@[protected, instance]
def sum.is_empty {α : Type u_1} {β : Type u_2} [is_empty α] [is_empty β] :
is_empty (α ⊕ β)
source
@[protected, instance]
def subtype.is_empty {α : Sort u_1} [is_empty α] (p : α → Prop) :
is_empty (subtype p)

subtypes of an empty type are empty

source
theorem subtype.is_empty_of_false {α : Sort u_1} {p : α → Prop} (hp : ∀ (a : α), ¬p a) :
is_empty (subtype p)

subtypes by an all-false predicate are false.

source
@[protected, instance]
def subtype.is_empty_false {α : Sort u_1} :
is_empty {a // false}

subtypes by false are false.

source
@[protected, instance]
def sigma.is_empty_left {α : Type u_1} [is_empty α] {E : α → Type u_2} :
is_empty (sigma E)
source
def is_empty_elim {α : Sort u_1} [is_empty α] {p : α → Sort u_2} (a : α) :
p a

Eliminate out of a type that is_empty (without using projection notation).

Equations
source
theorem is_empty_iff {α : Sort u_1} :
is_empty α ↔ α → false
source
@[protected]
def is_empty.elim {α : Sort u_1} (h : is_empty α) {p : α → Sort u_2} (a : α) :
p a

Eliminate out of a type that is_empty (using projection notation).

Equations
source
@[protected]
def is_empty.elim' {α : Sort u_1} {β : Sort u_2} (h : is_empty α) (a : α) :
β

Non-dependent version of is_empty.elim. Helpful if the elaborator cannot elaborate h.elim a correctly.

Equations
source
@[protected]
theorem is_empty.prop_iff {p : Prop} :
is_empty p ↔ ¬p
source
@[simp]
theorem is_empty.forall_iff {α : Sort u_1} [is_empty α] {p : α → Prop} :
(∀ (a : α), p a) ↔ true
source
@[simp]
theorem is_empty.exists_iff {α : Sort u_1} [is_empty α] {p : α → Prop} :
(∃ (a : α), p a) ↔ false
source
@[protected, instance]
def is_empty.subsingleton {α : Sort u_1} [is_empty α] :
subsingleton α
source
@[simp]
theorem not_nonempty_iff {α : Sort u_1} :
¬nonempty α ↔ is_empty α
source
@[simp]
theorem not_is_empty_iff {α : Sort u_1} :
¬is_empty α ↔ nonempty α
source
@[simp]
theorem is_empty_Prop {p : Prop} :
is_empty p ↔ ¬p
source
@[simp]
theorem is_empty_pi {α : Sort u_1} {π : α → Sort u_2} :
is_empty (Π (a : α), π a) ↔ ∃ (a : α), is_empty (π a)
source
@[simp]
theorem is_empty_sigma {α : Type u_1} {E : α → Type u_2} :
is_empty (sigma E) ↔ ∀ (a : α), is_empty (E a)
source
@[simp]
theorem is_empty_psigma {α : Sort u_1} {E : α → Sort u_2} :
is_empty (psigma E) ↔ ∀ (a : α), is_empty (E a)
source
@[simp]
theorem is_empty_subtype {α : Sort u_1} (p : α → Prop) :
is_empty (subtype p) ↔ ∀ (x : α), ¬p x
source
@[simp]
theorem is_empty_prod {α : Type u_1} {β : Type u_2} :
is_empty (α × β) ↔ is_empty α ∨ is_empty β
source
@[simp]
theorem is_empty_pprod {α : Sort u_1} {β : Sort u_2} :
is_empty (pprod α β) ↔ is_empty α ∨ is_empty β
source
@[simp]
theorem is_empty_sum {α : Type u_1} {β : Type u_2} :
is_empty (α ⊕ β) ↔ is_empty α ∧ is_empty β
source
@[simp]
theorem is_empty_psum {α : Sort u_1} {β : Sort u_2} :
is_empty (psum α β) ↔ is_empty α ∧ is_empty β
source
@[simp]
theorem is_empty_ulift {α : Type u_1} :
is_empty (ulift α) ↔ is_empty α
source
@[simp]
theorem is_empty_plift {α : Sort u_1} :
is_empty (plift α) ↔ is_empty α
source
theorem well_founded_of_empty {α : Sort u_1} [is_empty α] (r : α → α → Prop) :
well_founded r
source
theorem is_empty_or_nonempty (α : Sort u_1) :
is_empty α ∨ nonempty α
source
@[simp]
theorem not_is_empty_of_nonempty (α : Sort u_1) [h : nonempty α] :
¬is_empty α
source
theorem function.extend_of_empty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [is_empty α] (f : α → β) (g : α → γ) (h : β → γ) :
function.extend f g h = h