# 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.

source
class IsEmpty (α : Sort u_4) :
Prop

`IsEmpty α` expresses that `α` is empty.

- false : ∀ (a : α), False

Instances

source
instance Empty.instIsEmpty :
IsEmpty Empty
source
instance PEmpty.instIsEmpty :
IsEmpty PEmpty.{u_4}
source
instance instIsEmptyFalse :
IsEmpty False
source
instance Fin.isEmpty :
IsEmpty (Fin 0)
source
instance Fin.isEmpty' :
IsEmpty (Fin Nat.zero)
source
theorem Function.isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty β] (f : α → β) :
IsEmpty α
source
theorem Function.Surjective.isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] {f : α → β} (hf : Surjective f) :
IsEmpty β
source
instance instIsEmptyForallOfNonempty {α : Sort u_1} {p : α → Sort u_4} [∀ (x : α), IsEmpty (p x)] [h : Nonempty α] :
IsEmpty ((x : α) → p x)
source
instance PProd.isEmpty_left {α : Sort u_1} {β : Sort u_2} [IsEmpty α] :
IsEmpty (α ×' β)
source
instance PProd.isEmpty_right {α : Sort u_1} {β : Sort u_2} [IsEmpty β] :
IsEmpty (α ×' β)
source
instance Prod.isEmpty_left {α : Type u_4} {β : Type u_5} [IsEmpty α] :
IsEmpty (α × β)
source
instance Prod.isEmpty_right {α : Type u_4} {β : Type u_5} [IsEmpty β] :
IsEmpty (α × β)
source
instance Quot.instIsEmpty {α : Sort u_4} [IsEmpty α] {r : α → α → Prop} :
IsEmpty (Quot r)
source
instance Quotient.instIsEmpty {α : Sort u_4} [IsEmpty α] {s : Setoid α} :
IsEmpty (Quotient s)
source
instance instIsEmptyPSum {α : Sort u_1} {β : Sort u_2} [IsEmpty α] [IsEmpty β] :
IsEmpty (α ⊕' β)
source
instance instIsEmptySum {α : Type u_4} {β : Type u_5} [IsEmpty α] [IsEmpty β] :
IsEmpty (α ⊕ β)
source
instance instIsEmptySubtype {α : Sort u_1} [IsEmpty α] (p : α → Prop) :
IsEmpty (Subtype p)

subtypes of an empty type are empty

source
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.

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

subtypes by false are false.

source
instance Sigma.isEmpty_left {α : Type u_5} [IsEmpty α] {E : α → Type u_4} :
IsEmpty (Sigma E)
source
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

Instances For

source
theorem isEmpty_iff {α : Sort u_1} :
IsEmpty α ↔ ∀ (a : α), False
source
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

Instances For

source
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

Instances For

source
theorem IsEmpty.prop_iff {p : Prop} :
IsEmpty p ↔ ¬p
source
@[simp]
theorem IsEmpty.forall_iff {α : Sort u_1} [IsEmpty α] {p : α → Prop} :
(∀ (a : α), p a) ↔ True
source
@[simp]
theorem IsEmpty.exists_iff {α : Sort u_1} [IsEmpty α] {p : α → Prop} :
(∃ (a : α), p a) ↔ False
source
@[instance 100]
instance IsEmpty.instSubsingleton {α : Sort u_1} [IsEmpty α] :
Subsingleton α
source
@[simp]
theorem not_nonempty_iff {α : Sort u_1} :
¬Nonempty α ↔ IsEmpty α
source
@[simp]
theorem not_isEmpty_iff {α : Sort u_1} :
¬IsEmpty α ↔ Nonempty α
source
@[simp]
theorem isEmpty_Prop {p : Prop} :
IsEmpty p ↔ ¬p
source
@[simp]
theorem isEmpty_pi {α : Sort u_1} {π : α → Sort u_4} :
IsEmpty ((a : α) → π a) ↔ ∃ (a : α), IsEmpty (π a)
source
theorem isEmpty_fun {α : Sort u_1} {β : Sort u_2} :
IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
source
@[simp]
theorem nonempty_fun {α : Sort u_1} {β : Sort u_2} :
Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β
source
@[simp]
theorem isEmpty_sigma {α : Type u_5} {E : α → Type u_4} :
IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
source
@[simp]
theorem isEmpty_psigma {α : Sort u_5} {E : α → Sort u_4} :
IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
source
theorem isEmpty_subtype {α : Sort u_1} (p : α → Prop) :
IsEmpty (Subtype p) ↔ ∀ (x : α), ¬p x
source
@[simp]
theorem isEmpty_prod {α : Type u_4} {β : Type u_5} :
IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β
source
@[simp]
theorem isEmpty_pprod {α : Sort u_1} {β : Sort u_2} :
IsEmpty (α ×' β) ↔ IsEmpty α ∨ IsEmpty β
source
@[simp]
theorem isEmpty_sum {α : Type u_4} {β : Type u_5} :
IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
source
@[simp]
theorem isEmpty_psum {α : Sort u_4} {β : Sort u_5} :
IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β
source
@[simp]
theorem isEmpty_ulift {α : Type u_4} :
IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
source
@[simp]
theorem isEmpty_plift {α : Sort u_4} :
IsEmpty (PLift α) ↔ IsEmpty α
source
theorem wellFounded_of_isEmpty {α : Sort u_4} [IsEmpty α] (r : α → α → Prop) :
WellFounded r
source
theorem isEmpty_or_nonempty (α : Sort u_1) :
IsEmpty α ∨ Nonempty α
source
@[simp]
theorem not_isEmpty_of_nonempty (α : Sort u_1) [h : Nonempty α] :
¬IsEmpty α
source
theorem Function.extend_of_isEmpty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) :
extend f g h = h
source
@[simp]
theorem leftTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] :
Relator.LeftTotal R
source
theorem leftTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] :
Relator.LeftTotal R ↔ IsEmpty α
source
@[simp]
theorem rightTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] :
Relator.RightTotal R
source
theorem rightTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] :
Relator.RightTotal R ↔ IsEmpty β
source
@[simp]
theorem biTotal_empty {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] [IsEmpty β] :
Relator.BiTotal R
source
theorem biTotal_iff_isEmpty_right {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α] :
Relator.BiTotal R ↔ IsEmpty β
source
theorem biTotal_iff_isEmpty_left {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty β] :
Relator.BiTotal R ↔ IsEmpty α
source
theorem Function.Bijective.of_isEmpty {α : Type u_4} {β : Type u_5} (f : α → β) [IsEmpty β] :
Bijective f