Documentation

Mathlib.Basic.IsEmpty.Defs

Types that are empty #

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

Main declaration #

source
class IsEmpty (α : Sort u) :
Prop

IsEmpty α expresses that α is empty.

  • false : ∀ (a : α), False
Instances
    source
    instance Empty.instIsEmpty :
    IsEmpty Empty
    source
    instance PEmpty.instIsEmpty :
    IsEmpty PEmpty
    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} {β : Sort v} [IsEmpty β] (f : α → β) :
    IsEmpty α
    source
    theorem Function.Surjective.isEmpty {α : Sort u} {β : Sort v} [IsEmpty α] {f : α → β} (hf : Surjective f) :
    IsEmpty β
    source
    instance instIsEmptyForallOfNonempty {α : Sort u} {p : α → Sort v} [∀ (x : α), IsEmpty (p x)] [h : Nonempty α] :
    IsEmpty ((x : α) → p x)
    source
    instance PProd.isEmpty_left {α : Sort u} {β : Sort v} [IsEmpty α] :
    IsEmpty (α ×' β)
    source
    instance PProd.isEmpty_right {α : Sort u} {β : Sort v} [IsEmpty β] :
    IsEmpty (α ×' β)
    source
    instance Prod.isEmpty_left {α : Type u_1} {β : Type u_2} [IsEmpty α] :
    IsEmpty (α × β)
    source
    instance Prod.isEmpty_right {α : Type u_1} {β : Type u_2} [IsEmpty β] :
    IsEmpty (α × β)
    source
    instance Quot.instIsEmpty {α : Sort u} [IsEmpty α] {r : α → α → Prop} :
    IsEmpty (Quot r)
    source
    instance Quotient.instIsEmpty {α : Sort u} [IsEmpty α] {s : Setoid α} :
    IsEmpty (Quotient s)
    source
    instance instIsEmptyPSum {α : Sort u} {β : Sort v} [IsEmpty α] [IsEmpty β] :
    IsEmpty (α ⊕' β)
    source
    instance instIsEmptySum {α : Type u_1} {β : Type u_2} [IsEmpty α] [IsEmpty β] :
    IsEmpty (α ⊕ β)
    source
    instance instIsEmptySubtype {α : Sort u} [IsEmpty α] (p : α → Prop) :
    IsEmpty (Subtype p)

    Subtypes of an empty type are empty.

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

    Subtypes by an all-false predicate are empty.

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

    Subtypes by False are empty.

    source
    instance Sigma.isEmpty_left {α : Type u_1} [IsEmpty α] {E : α → Type v} :
    IsEmpty (Sigma E)
    source
    instance Sigma.isEmpty_fibers {α : Type u_1} {E : α → Type v} [∀ (a : α), IsEmpty (E a)] :
    IsEmpty (Sigma E)
    source
    def isEmptyElim {α : Sort u} [IsEmpty α] {p : α → Sort v} (a : α) :
    p a

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

    Instances For
      source
      theorem isEmpty_iff {α : Sort u} :
      IsEmpty α ↔ ∀ (a : α), False
      source
      def IsEmpty.elim {α : Sort u} :
      IsEmpty α → {p : α → Sort v} → (a : α) → p a

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

      Instances For
        source
        def IsEmpty.elim' {α : Sort u} {β : Sort v} (h : IsEmpty α) (a : α) :
        β

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

        Instances For
          source
          theorem IsEmpty.prop_iff {p : Prop} :
          IsEmpty p ↔ ¬p
          source
          @[simp]
          theorem IsEmpty.forall_iff {α : Sort u} [IsEmpty α] {p : α → Prop} :
          (∀ (a : α), p a) ↔ True
          source
          @[simp]
          theorem IsEmpty.exists_iff {α : Sort u} [IsEmpty α] {p : α → Prop} :
          (∃ (a : α), p a) ↔ False
          source
          @[instance 100]
          instance IsEmpty.subsingleton {α : Sort u} [IsEmpty α] :
          Subsingleton α
          source
          theorem IsEmpty.congr_fun {α : Sort u} {β : Sort v} [IsEmpty α] (f g : α → β) :
          f = g
          source
          @[simp]
          theorem Fin.isEmpty_iff {k : Nat} :
          IsEmpty (Fin k) ↔ k = 0

          Fin k is empty iff k = 0.