Types that are empty

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

Main declaration

• IsEmpty: a typeclass that expresses that a type is empty.

class IsEmpty (α : Sort u_4) : Prop

IsEmpty α expresses that α is empty.

• false : ∀ (a : α), False

instance Empty.instIsEmpty : IsEmpty Empty

instance PEmpty.instIsEmpty : IsEmpty PEmpty.{u_4}

instance instIsEmptyFalse : IsEmpty False

instance Fin.isEmpty : IsEmpty (Fin 0)

instance Fin.isEmpty' : IsEmpty (Fin Nat.zero)

theorem Function.isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty β] (f : α → β) : IsEmpty α

theorem Function.Surjective.isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] {f : α → β} (hf : Surjective f) : IsEmpty β

instance instIsEmptyForallOfNonempty {α : Sort u_1} {p : α → Sort u_4} [∀ (x : α), IsEmpty (p x)] [h : Nonempty α] : IsEmpty ((x : α) → p x)

instance PProd.isEmpty_left {α : Sort u_1} {β : Sort u_2} [IsEmpty α] : IsEmpty (α ×' β)

instance PProd.isEmpty_right {α : Sort u_1} {β : Sort u_2} [IsEmpty β] : IsEmpty (α ×' β)

instance Prod.isEmpty_left {α : Type u_4} {β : Type u_5} [IsEmpty α] : IsEmpty (α × β)

instance Prod.isEmpty_right {α : Type u_4} {β : Type u_5} [IsEmpty β] : IsEmpty (α × β)

instance Quot.instIsEmpty {α : Sort u_4} [IsEmpty α] {r : α → α → Prop} : IsEmpty (Quot r)

instance Quotient.instIsEmpty {α : Sort u_4} [IsEmpty α] {s : Setoid α} : IsEmpty (Quotient s)

instance instIsEmptyPSum {α : Sort u_1} {β : Sort u_2} [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕' β)

instance instIsEmptySum {α : Type u_4} {β : Type u_5} [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕ β)

instance instIsEmptySubtype {α : Sort u_1} [IsEmpty α] (p : α → Prop) : IsEmpty (Subtype p)

subtypes of an empty type are empty

theorem Subtype.isEmpty_of_false {α : Sort u_1} {p : α → Prop} (hp : ∀ (a : α), ¬p a) : IsEmpty (Subtype p)

subtypes by an all-false predicate are false.

instance Subtype.isEmpty_false {α : Sort u_1} : IsEmpty { _a : α // False }

subtypes by false are false.

instance Sigma.isEmpty_left {α : Type u_5} [IsEmpty α] {E : α → Type u_4} : IsEmpty (Sigma E)

def isEmptyElim {α : Sort u_1} [IsEmpty α] {p : α → Sort u_4} (a : α) : p a

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

Equations

• isEmptyElim a = ⋯.elim

theorem isEmpty_iff {α : Sort u_1} : IsEmpty α ↔ ∀ (a : α), False

def IsEmpty.elim {α : Sort u} : IsEmpty α → {p : α → Sort u_4} → (a : α) → p a

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

Equations

• x✝.elim a = isEmptyElim a

def IsEmpty.elim' {α : Sort u_1} {β : Sort u_4} (h : IsEmpty α) (a : α) : β

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

Equations

• h.elim' a = ⋯.elim

theorem IsEmpty.prop_iff {p : Prop} : IsEmpty p ↔ ¬p

@[simp]

theorem IsEmpty.forall_iff {α : Sort u_1} [IsEmpty α] {p : α → Prop} : (∀ (a : α), p a) ↔ True

@[simp]

theorem IsEmpty.exists_iff {α : Sort u_1} [IsEmpty α] {p : α → Prop} : (∃ (a : α), p a) ↔ False

@[instance 100]

instance IsEmpty.instSubsingleton {α : Sort u_1} [IsEmpty α] : Subsingleton α

@[simp]

theorem not_nonempty_iff {α : Sort u_1} : ¬Nonempty α ↔ IsEmpty α

@[simp]

theorem not_isEmpty_iff {α : Sort u_1} : ¬IsEmpty α ↔ Nonempty α

@[simp]

theorem isEmpty_Prop {p : Prop} : IsEmpty p ↔ ¬p

@[simp]

theorem isEmpty_pi {α : Sort u_1} {π : α → Sort u_4} : IsEmpty ((a : α) → π a) ↔ ∃ (a : α), IsEmpty (π a)

theorem isEmpty_fun {α : Sort u_1} {β : Sort u_2} : IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

@[simp]

theorem nonempty_fun {α : Sort u_1} {β : Sort u_2} : Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β

@[simp]

theorem isEmpty_sigma {α : Type u_5} {E : α → Type u_4} : IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)

@[simp]

theorem isEmpty_psigma {α : Sort u_5} {E : α → Sort u_4} : IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)

theorem isEmpty_subtype {α : Sort u_1} (p : α → Prop) : IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x

@[simp]

theorem isEmpty_prod {α : Type u_4} {β : Type u_5} : IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

@[simp]

theorem isEmpty_pprod {α : Sort u_1} {β : Sort u_2} : IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β

@[simp]

theorem isEmpty_sum {α : Type u_4} {β : Type u_5} : IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

@[simp]

theorem isEmpty_psum {α : Sort u_4} {β : Sort u_5} : IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

@[simp]

theorem isEmpty_ulift {α : Type u_4} : IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α

@[simp]

theorem isEmpty_plift {α : Sort u_4} : IsEmpty (PLift α) ↔ IsEmpty α

theorem wellFounded_of_isEmpty {α : Sort u_4} [IsEmpty α] (r : α → α → Prop) : WellFounded r

theorem isEmpty_or_nonempty (α : Sort u_1) : IsEmpty α ∨ Nonempty α

@[simp]

theorem not_isEmpty_of_nonempty (α : Sort u_1) [h : Nonempty α] : ¬IsEmpty α

theorem Function.extend_of_isEmpty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) : extend f g h = h

@[simp]

theorem leftTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.LeftTotal R

theorem leftTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.LeftTotal R ↔ IsEmpty α

@[simp]

theorem rightTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.RightTotal R

theorem rightTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.RightTotal R ↔ IsEmpty β

@[simp]

theorem biTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] [IsEmpty β] : Relator.BiTotal R

theorem biTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] : Relator.BiTotal R ↔ IsEmpty β

theorem biTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] : Relator.BiTotal R ↔ IsEmpty α

theorem Function.Bijective.of_isEmpty {α : Type u_4} {β : Type u_5} (f : α → β) [IsEmpty β] : Bijective f