Documentation

Mathlib.Logic.IsEmpty

Types that are empty #

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

Main declaration #

class IsEmpty (α : Sort u_1) :

IsEmpty α expresses that α is empty.

Instances
    theorem Function.isEmpty {α : Sort u_2} {β : Sort u_1} [inst : IsEmpty β] (f : αβ) :
    instance instIsEmptyForAll {α : Sort u_1} {p : αSort u_2} [h : Nonempty α] [inst : ∀ (x : α), IsEmpty (p x)] :
    IsEmpty ((x : α) → p x)
    Equations
    instance PProd.isEmpty_left {α : Sort u_1} {β : Sort u_2} [inst : IsEmpty α] :
    IsEmpty (PProd α β)
    Equations
    instance Prod.isEmpty_left {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] :
    IsEmpty (α × β)
    Equations
    instance Prod.isEmpty_right {α : Type u_1} {β : Type u_2} [inst : IsEmpty β] :
    IsEmpty (α × β)
    Equations
    instance instIsEmptyPSum {α : Sort u_1} {β : Sort u_2} [inst : IsEmpty α] [inst : IsEmpty β] :
    IsEmpty (α ⊕' β)
    Equations
    instance instIsEmptySum {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] [inst : IsEmpty β] :
    IsEmpty (α β)
    Equations
    instance instIsEmptySubtype {α : Sort u_1} [inst : IsEmpty α] (p : αProp) :

    subtypes of an empty type are empty

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

    subtypes by an all-false predicate are false.

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

    subtypes by false are false.

    Equations
    instance Sigma.isEmpty_left {α : Type u_1} [inst : IsEmpty α] {E : αType u_2} :
    Equations
    def isEmptyElim {α : Sort u_1} [inst : IsEmpty α] {p : αSort u_2} (a : α) :
    p a

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

    Equations
    theorem isEmpty_iff {α : Sort u_1} :
    IsEmpty α αFalse
    def IsEmpty.elim {α : Sort u} :
    IsEmpty α{p : αSort u_1} → (a : α) → p a

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

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

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

    Equations
    @[simp]
    theorem IsEmpty.forall_iff {α : Sort u_1} [inst : IsEmpty α] {p : αProp} :
    ((a : α) → p a) True
    @[simp]
    theorem IsEmpty.exists_iff {α : Sort u_1} [inst : IsEmpty α] {p : αProp} :
    (a, p a) False
    @[simp]
    theorem not_nonempty_iff {α : Sort u_1} :
    @[simp]
    theorem not_isEmpty_iff {α : Sort u_1} :
    @[simp]
    theorem isEmpty_Prop {p : Prop} :
    @[simp]
    theorem isEmpty_pi {α : Sort u_2} {π : αSort u_1} :
    IsEmpty ((a : α) → π a) a, IsEmpty (π a)
    @[simp]
    theorem isEmpty_sigma {α : Type u_1} {E : αType u_2} :
    IsEmpty (Sigma E) ∀ (a : α), IsEmpty (E a)
    @[simp]
    theorem isEmpty_psigma {α : Sort u_1} {E : αSort u_2} :
    IsEmpty (PSigma E) ∀ (a : α), IsEmpty (E a)
    @[simp]
    theorem isEmpty_subtype {α : Sort u_1} (p : αProp) :
    IsEmpty (Subtype p) ∀ (x : α), ¬p x
    @[simp]
    theorem isEmpty_prod {α : Type u_1} {β : Type u_2} :
    @[simp]
    theorem isEmpty_pprod {α : Sort u_2} {β : Sort u_1} :
    @[simp]
    theorem isEmpty_sum {α : Type u_1} {β : Type u_2} :
    @[simp]
    theorem isEmpty_psum {α : Sort u_1} {β : Sort u_2} :
    @[simp]
    theorem isEmpty_ulift {α : Type u_1} :
    @[simp]
    theorem isEmpty_plift {α : Sort u_1} :
    theorem wellFounded_of_isEmpty {α : Sort u_1} [inst : IsEmpty α] (r : ααProp) :
    @[simp]
    theorem not_isEmpty_of_nonempty (α : Sort u_1) [h : Nonempty α] :
    theorem Function.extend_of_isEmpty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [inst : IsEmpty α] (f : αβ) (g : αγ) (h : βγ) :