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_4) :

IsEmpty α expresses that α is empty.

Instances
    theorem Function.isEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty β] (f : αβ) :
    instance instIsEmptyForAll {α : Sort u_1} {p : αSort u_4} [h : Nonempty α] [∀ (x : α), IsEmpty (p x)] :
    IsEmpty ((x : α) → p x)
    Equations
    instance instIsEmptyPSum {α : Sort u_1} {β : Sort u_2} [IsEmpty α] [IsEmpty β] :
    IsEmpty (α ⊕' β)
    Equations
    instance instIsEmptySum {α : Type u_4} {β : Type u_5} [IsEmpty α] [IsEmpty β] :
    IsEmpty (α β)
    Equations
    instance instIsEmptySubtype {α : Sort u_1} [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
    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
    Instances For
      theorem isEmpty_iff {α : Sort u_1} :
      IsEmpty α α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
      Instances For
        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
        Instances For
          @[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
          @[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_1} {π : αSort u_4} :
          IsEmpty ((a : α) → π a) a, IsEmpty (π a)
          @[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)
          @[simp]
          theorem isEmpty_subtype {α : Sort u_1} (p : αProp) :
          IsEmpty (Subtype p) ∀ (x : α), ¬p x
          @[simp]
          theorem isEmpty_prod {α : Type u_4} {β : Type u_5} :
          @[simp]
          theorem isEmpty_pprod {α : Sort u_1} {β : Sort u_2} :
          @[simp]
          theorem isEmpty_sum {α : Type u_4} {β : Type u_5} :
          @[simp]
          theorem isEmpty_psum {α : Sort u_4} {β : Sort u_5} :
          @[simp]
          @[simp]
          theorem isEmpty_plift {α : Sort u_4} :
          theorem wellFounded_of_isEmpty {α : Sort u_4} [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} [IsEmpty α] (f : αβ) (g : αγ) (h : βγ) :