mathlib3 documentation

logic.is_empty

Types that are empty #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declaration #

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def fin.is_empty  :
@[protected]
theorem function.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty β] (f : α β) :
@[protected, instance]
def pi.is_empty {α : Sort u_1} {p : α Sort u_2} [h : nonempty α] [ (x : α), is_empty (p x)] :
is_empty (Π (x : α), p x)
@[protected, instance]
def pprod.is_empty_left {α : Sort u_1} {β : Sort u_2} [is_empty α] :
is_empty (pprod α β)
@[protected, instance]
def pprod.is_empty_right {α : Sort u_1} {β : Sort u_2} [is_empty β] :
is_empty (pprod α β)
@[protected, instance]
def prod.is_empty_left {α : Type u_1} {β : Type u_2} [is_empty α] :
is_empty × β)
@[protected, instance]
def prod.is_empty_right {α : Type u_1} {β : Type u_2} [is_empty β] :
is_empty × β)
@[protected, instance]
def psum.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty α] [is_empty β] :
is_empty (psum α β)
@[protected, instance]
def sum.is_empty {α : Type u_1} {β : Type u_2} [is_empty α] [is_empty β] :
is_empty β)
@[protected, instance]
def subtype.is_empty {α : Sort u_1} [is_empty α] (p : α Prop) :

subtypes of an empty type are empty

theorem subtype.is_empty_of_false {α : Sort u_1} {p : α Prop} (hp : (a : α), ¬p a) :

subtypes by an all-false predicate are false.

@[protected, instance]
def subtype.is_empty_false {α : Sort u_1} :

subtypes by false are false.

@[protected, instance]
def sigma.is_empty_left {α : Type u_1} [is_empty α] {E : α Type u_2} :
def is_empty_elim {α : Sort u_1} [is_empty α] {p : α Sort u_2} (a : α) :
p a

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

Equations
theorem is_empty_iff {α : Sort u_1} :
@[protected]
def is_empty.elim {α : Sort u_1} (h : is_empty α) {p : α Sort u_2} (a : α) :
p a

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

Equations
@[protected]
def is_empty.elim' {α : Sort u_1} {β : Sort u_2} (h : is_empty α) (a : α) :
β

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

Equations
@[protected]
theorem is_empty.prop_iff {p : Prop} :
@[simp]
theorem is_empty.forall_iff {α : Sort u_1} [is_empty α] {p : α Prop} :
( (a : α), p a) true
@[simp]
theorem is_empty.exists_iff {α : Sort u_1} [is_empty α] {p : α Prop} :
( (a : α), p a) false
@[protected, instance]
def is_empty.subsingleton {α : Sort u_1} [is_empty α] :
@[simp]
theorem not_nonempty_iff {α : Sort u_1} :
@[simp]
theorem not_is_empty_iff {α : Sort u_1} :
@[simp]
theorem is_empty_Prop {p : Prop} :
@[simp]
theorem is_empty_pi {α : Sort u_1} {π : α Sort u_2} :
is_empty (Π (a : α), π a) (a : α), is_empty (π a)
@[simp]
theorem is_empty_sigma {α : Type u_1} {E : α Type u_2} :
is_empty (sigma E) (a : α), is_empty (E a)
@[simp]
theorem is_empty_psigma {α : Sort u_1} {E : α Sort u_2} :
is_empty (psigma E) (a : α), is_empty (E a)
@[simp]
theorem is_empty_subtype {α : Sort u_1} (p : α Prop) :
is_empty (subtype p) (x : α), ¬p x
@[simp]
theorem is_empty_prod {α : Type u_1} {β : Type u_2} :
@[simp]
theorem is_empty_pprod {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem is_empty_sum {α : Type u_1} {β : Type u_2} :
@[simp]
theorem is_empty_psum {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem is_empty_ulift {α : Type u_1} :
@[simp]
theorem is_empty_plift {α : Sort u_1} :
theorem well_founded_of_empty {α : Sort u_1} [is_empty α] (r : α α Prop) :
theorem is_empty_or_nonempty (α : Sort u_1) :
@[simp]
theorem not_is_empty_of_nonempty (α : Sort u_1) [h : nonempty α] :
theorem function.extend_of_empty {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} [is_empty α] (f : α β) (g : α γ) (h : β γ) :