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 : α → False

Instances

source

instance instIsEmptyEmpty :

IsEmpty Empty

Equations

instIsEmptyEmpty = (_ : IsEmpty Empty)

source

instance instIsEmptyPEmpty :

IsEmpty PEmpty.{u_4}

Equations

instIsEmptyPEmpty = (_ : IsEmpty PEmpty.{u_4})

source

instance instIsEmptyFalse :

IsEmpty False

Equations

instIsEmptyFalse = (_ : IsEmpty False)

source

instance Fin.isEmpty :

IsEmpty (Fin 0)

Equations

Fin.isEmpty = (_ : IsEmpty (Fin 0))

source

instance Fin.isEmpty' :

IsEmpty (Fin Nat.zero)

Equations

Fin.isEmpty' = Fin.isEmpty

source

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

IsEmpty α

source

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

IsEmpty ((x : α) → p x)

Equations

(_ : IsEmpty ((x : α) → p x)) = (_ : IsEmpty ((x : α) → p x))

source

instance PProd.isEmpty_left {α : Sort u_1} {β : Sort u_2} [IsEmpty α] :

IsEmpty (PProd α β)

Equations

(_ : IsEmpty (PProd α β)) = (_ : IsEmpty (PProd α β))

source

instance PProd.isEmpty_right {α : Sort u_1} {β : Sort u_2} [IsEmpty β] :

IsEmpty (PProd α β)

Equations

(_ : IsEmpty (PProd α β)) = (_ : IsEmpty (PProd α β))

source

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

IsEmpty (α × β)

Equations

(_ : IsEmpty (α × β)) = (_ : IsEmpty (α × β))

source

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

IsEmpty (α × β)

Equations

(_ : IsEmpty (α × β)) = (_ : IsEmpty (α × β))

source

instance instIsEmptyPSum {α : Sort u_1} {β : Sort u_2} [IsEmpty α] [IsEmpty β] :

IsEmpty (α ⊕' β)

Equations

(_ : IsEmpty (α ⊕' β)) = (_ : IsEmpty (α ⊕' β))

source

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

IsEmpty (α ⊕ β)

Equations

(_ : IsEmpty (α ⊕ β)) = (_ : IsEmpty (α ⊕ β))

source

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

IsEmpty (Subtype p)

subtypes of an empty type are empty

Equations

(_ : IsEmpty (Subtype p)) = (_ : IsEmpty (Subtype p))

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.

Equations

(_ : IsEmpty { _a : α // False }) = (_ : IsEmpty { _a : α // False })

source

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

IsEmpty (Sigma E)

Equations

(_ : IsEmpty (Sigma E)) = (_ : 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 = (_ : False).elim

Instances For

source

theorem isEmpty_iff {α : Sort u_1} :

IsEmpty α ↔ α → 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

IsEmpty.elim x 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

IsEmpty.elim' h a = (_ : False).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 IsEmpty.instSubsingleton {α : Sort u_1} [IsEmpty α] :

Subsingleton α

Equations

(_ : Subsingleton α) = (_ : 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

@[simp]

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

@[simp]

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 (PProd α β) ↔ 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 : β → γ) :

Function.extend f g h = h

Documentation

Mathlib.Logic.IsEmpty

Types that are empty #

Main declaration #