mathlib documentation

logic.is_empty

Types that are empty #

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

Main declaration #

@[instance]
@[instance]
@[instance]
@[instance]
def fin.is_empty  :
theorem function.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty β] (f : α → β) :
@[instance]
def pi.is_empty {α : Sort u_1} {p : α → Sort u_2} [h : nonempty α] [∀ (x : α), is_empty (p x)] :
is_empty (Π (x : α), p x)
@[instance]
def pprod.is_empty_left {α : Sort u_1} {β : Sort u_2} [is_empty α] :
is_empty (pprod α β)
@[instance]
def pprod.is_empty_right {α : Sort u_1} {β : Sort u_2} [is_empty β] :
is_empty (pprod α β)
@[instance]
def prod.is_empty_left {α : Type u_1} {β : Type u_2} [is_empty α] :
is_empty × β)
@[instance]
def prod.is_empty_right {α : Type u_1} {β : Type u_2} [is_empty β] :
is_empty × β)
@[instance]
def psum.is_empty {α : Sort u_1} {β : Sort u_2} [is_empty α] [is_empty β] :
is_empty (psum α β)
@[instance]
def sum.is_empty {α : Type u_1} {β : Type u_2} [is_empty α] [is_empty β] :
is_empty β)
@[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.

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

subtypes by false are false.

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} :
is_empty α α → false
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
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
theorem is_empty.prop_iff {p : Prop} :
theorem is_empty.forall_iff {α : Sort u_1} [is_empty α] {p : α → Prop} :
(∀ (a : α), p a) true
theorem is_empty.exists_iff {α : Sort u_1} [is_empty α] {p : α → Prop} :
(∃ (a : α), p a) false
@[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_pi {α : Sort u_1} {π : α → Sort u_2} :
is_empty (Π (a : α), «π» a) ∃ (a : α), is_empty («π» a)
@[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} :
theorem is_empty_or_nonempty (α : Sort u_1) :
@[simp]
theorem not_is_empty_of_nonempty (α : Sort u_1) [h : nonempty α] :