Mathlib.Logic.IsEmpty

IsEmpty structure

(α : Sort*)

Full source

/-- `IsEmpty α` expresses that `α` is empty. -/
class IsEmpty (α : Sort*) : Prop where
  protected false : α → False

Empty type

Informal description

The structure `IsEmpty α` expresses that the type `α` has no elements.

Empty.instIsEmpty instance

: IsEmpty Empty

Full source

instance Empty.instIsEmpty : IsEmpty Empty :=
  ⟨Empty.elim⟩

The Empty Type is Empty

Informal description

The empty type `Empty` has no elements.

PEmpty.instIsEmpty instance

: IsEmpty PEmpty

Full source

instance PEmpty.instIsEmpty : IsEmpty PEmpty :=
  ⟨PEmpty.elim⟩

`PEmpty` is Empty

Informal description

The type `PEmpty` is empty.

instIsEmptyFalse instance

: IsEmpty False

Full source

instance : IsEmpty False :=
  ⟨id⟩

`False` is Empty

Informal description

The type `False` is empty.

Fin.isEmpty instance

: IsEmpty (Fin 0)

Full source

instance Fin.isEmpty : IsEmpty (Fin 0) :=
  ⟨fun n ↦ Nat.not_lt_zero n.1 n.2⟩

The Fin 0 Type is Empty

Informal description

The type $\mathrm{Fin}\,0$ is empty.

Fin.isEmpty' instance

: IsEmpty (Fin Nat.zero)

Full source

instance Fin.isEmpty' : IsEmpty (Fin Nat.zero) :=
  Fin.isEmpty

The Fin 0 Type is Empty

Informal description

The type $\mathrm{Fin}\,0$ is empty.

Function.isEmpty theorem

[IsEmpty β] (f : α → β) : IsEmpty α

Full source

protected theorem Function.isEmpty [IsEmpty β] (f : α → β) : IsEmpty α :=
  ⟨fun x ↦ IsEmpty.false (f x)⟩

Empty codomain implies empty domain

Informal description

If $\beta$ is an empty type and $f \colon \alpha \to \beta$ is a function, then $\alpha$ is also an empty type.

Function.Surjective.isEmpty theorem

[IsEmpty α] {f : α → β} (hf : f.Surjective) : IsEmpty β

Full source

theorem Function.Surjective.isEmpty [IsEmpty α] {f : α → β} (hf : f.Surjective) : IsEmpty β :=
  ⟨fun y ↦ let ⟨x, _⟩ := hf y; IsEmpty.false x⟩

Surjective Function from Empty Type Implies Empty Codomain

Informal description

If $\alpha$ is an empty type and $f \colon \alpha \to \beta$ is a surjective function, then $\beta$ is also an empty type.

instIsEmptyForallOfNonempty instance

{p : α → Sort*} [∀ x, IsEmpty (p x)] [h : Nonempty α] : IsEmpty (∀ x, p x)

Full source

instance {p : α → Sort*} [∀ x, IsEmpty (p x)] [h : Nonempty α] : IsEmpty (∀ x, p x) :=
  h.elim fun x ↦ Function.isEmpty <| Function.eval x

Empty Dependent Function Type from Nonempty Domain and Empty Codomains

Informal description

For any type $\alpha$ and a family of types $p : \alpha \to \text{Sort*}$, if each $p(x)$ is empty and $\alpha$ is nonempty, then the type of dependent functions $\forall x, p(x)$ is empty.

PProd.isEmpty_left instance

[IsEmpty α] : IsEmpty (PProd α β)

Full source

instance PProd.isEmpty_left [IsEmpty α] : IsEmpty (PProd α β) :=
  Function.isEmpty PProd.fst

Empty Left Type Implies Empty Dependent Pair Type

Informal description

If $\alpha$ is an empty type, then the type of dependent pairs $\text{PProd}\ \alpha\ \beta$ is also empty for any type $\beta$.

PProd.isEmpty_right instance

[IsEmpty β] : IsEmpty (PProd α β)

Full source

instance PProd.isEmpty_right [IsEmpty β] : IsEmpty (PProd α β) :=
  Function.isEmpty PProd.snd

Empty Right Type Implies Empty Dependent Pair Type

Informal description

For any type $\beta$, if $\beta$ is empty, then the dependent pair type $\text{PProd}\ \alpha\ \beta$ is also empty for any type $\alpha$.

Prod.isEmpty_left instance

{α β} [IsEmpty α] : IsEmpty (α × β)

Full source

instance Prod.isEmpty_left {α β} [IsEmpty α] : IsEmpty (α × β) :=
  Function.isEmpty Prod.fst

Empty Left Component Implies Empty Product Type

Informal description

For any types $\alpha$ and $\beta$, if $\alpha$ is empty, then the product type $\alpha \times \beta$ is also empty.

Prod.isEmpty_right instance

{α β} [IsEmpty β] : IsEmpty (α × β)

Full source

instance Prod.isEmpty_right {α β} [IsEmpty β] : IsEmpty (α × β) :=
  Function.isEmpty Prod.snd

Empty Right Component Implies Empty Product Type

Informal description

For any types $\alpha$ and $\beta$, if $\beta$ is empty, then the product type $\alpha \times \beta$ is also empty.

Quot.instIsEmpty instance

{α : Sort*} [IsEmpty α] {r : α → α → Prop} : IsEmpty (Quot r)

Full source

instance Quot.instIsEmpty {α : Sort*} [IsEmpty α] {r : α → α → Prop} : IsEmpty (Quot r) :=
  Function.Surjective.isEmpty Quot.exists_rep

Quotient of Empty Type is Empty

Informal description

For any empty type $\alpha$ and any relation $r$ on $\alpha$, the quotient type $\mathrm{Quot}\, r$ is also empty.

Quotient.instIsEmpty instance

{α : Sort*} [IsEmpty α] {s : Setoid α} : IsEmpty (Quotient s)

Full source

instance Quotient.instIsEmpty {α : Sort*} [IsEmpty α] {s : Setoid α} : IsEmpty (Quotient s) :=
  Quot.instIsEmpty

Quotient of Empty Type is Empty

Informal description

For any empty type $\alpha$ and any setoid $s$ on $\alpha$, the quotient type $\mathrm{Quotient}\, s$ is also empty.

instIsEmptyPSum instance

[IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕' β)

Full source

instance [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕' β) :=
  ⟨fun x ↦ PSum.rec IsEmpty.false IsEmpty.false x⟩

Psum of Empty Types is Empty

Informal description

For any two empty types $\alpha$ and $\beta$, their psum (the universe-polymorphic sum type) $\alpha \oplus' \beta$ is also empty.

instIsEmptySum instance

{α β} [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕ β)

Full source

instance instIsEmptySum {α β} [IsEmpty α] [IsEmpty β] : IsEmpty (α ⊕ β) :=
  ⟨fun x ↦ Sum.rec IsEmpty.false IsEmpty.false x⟩

Sum of Empty Types is Empty

Informal description

For any two empty types $\alpha$ and $\beta$, their sum type $\alpha \oplus \beta$ is also empty.

instIsEmptySubtype instance

[IsEmpty α] (p : α → Prop) : IsEmpty (Subtype p)

Full source

/-- subtypes of an empty type are empty -/
instance [IsEmpty α] (p : α → Prop) : IsEmpty (Subtype p) :=
  ⟨fun x ↦ IsEmpty.false x.1⟩

Subtypes of Empty Types are Empty

Informal description

For any empty type $\alpha$ and predicate $p : \alpha \to \text{Prop}$, the subtype $\{a \in \alpha \mid p(a)\}$ is also empty.

Subtype.isEmpty_of_false theorem

{p : α → Prop} (hp : ∀ a, ¬p a) : IsEmpty (Subtype p)

Full source

/-- subtypes by an all-false predicate are false. -/
theorem Subtype.isEmpty_of_false {p : α → Prop} (hp : ∀ a, ¬p a) : IsEmpty (Subtype p) :=
  ⟨fun x ↦ hp _ x.2⟩

Empty Subtype from False Predicate

Informal description

For any type $\alpha$ and predicate $p : \alpha \to \text{Prop}$, if for every element $a$ of $\alpha$ the proposition $p(a)$ is false, then the subtype $\{a \in \alpha \mid p(a)\}$ is empty.

Subtype.isEmpty_false instance

: IsEmpty { _a : α // False }

Full source

/-- subtypes by false are false. -/
instance Subtype.isEmpty_false : IsEmpty { _a : α // False } :=
  Subtype.isEmpty_of_false fun _ ↦ id

Empty Subtype from False Condition

Informal description

For any type $\alpha$, the subtype $\{a \in \alpha \mid \text{False}\}$ is empty.

Sigma.isEmpty_left instance

{α} [IsEmpty α] {E : α → Type*} : IsEmpty (Sigma E)

Full source

instance Sigma.isEmpty_left {α} [IsEmpty α] {E : α → Type*} : IsEmpty (Sigma E) :=
  Function.isEmpty Sigma.fst

Dependent Sum of Empty Type is Empty

Informal description

For any empty type $\alpha$ and any type family $E : \alpha \to \text{Type}$, the dependent sum type $\Sigma (a : \alpha), E(a)$ is also empty.

isEmptyElim definition

[IsEmpty α] {p : α → Sort*} (a : α) : p a

Full source

/-- Eliminate out of a type that `IsEmpty` (without using projection notation). -/
@[elab_as_elim]
def isEmptyElim [IsEmpty α] {p : α → Sort*} (a : α) : p a :=
  (IsEmpty.false a).elim

Vacuous elimination for empty types

Informal description

Given a type $\alpha$ that is empty (i.e., has no elements) and a dependent type family $p : \alpha \to \text{Sort}*$, the function `isEmptyElim` takes an element $a : \alpha$ (which cannot exist) and returns a term of type $p a$. This is a vacuous elimination principle for empty types.

isEmpty_iff theorem

: IsEmpty α ↔ α → False

Full source

theorem isEmpty_iff : IsEmptyIsEmpty α ↔ α → False :=
  ⟨@IsEmpty.false α, IsEmpty.mk⟩

Characterization of Empty Types

Informal description

A type $\alpha$ is empty if and only if every element of $\alpha$ implies false, i.e., $\text{IsEmpty}(\alpha) \leftrightarrow (\forall x \in \alpha, \text{False})$.

IsEmpty.elim definition

{α : Sort u} (_ : IsEmpty α) {p : α → Sort*} (a : α) : p a

Full source

/-- Eliminate out of a type that `IsEmpty` (using projection notation). -/
@[elab_as_elim]
protected def elim {α : Sort u} (_ : IsEmpty α) {p : α → Sort*} (a : α) : p a :=
  isEmptyElim a

Vacuous elimination for empty types

Informal description

Given a type $\alpha$ that is empty (i.e., has no elements) and a dependent type family $p : \alpha \to \text{Sort}*$, the function takes an element $a : \alpha$ (which cannot exist) and returns a term of type $p a$. This is a vacuous elimination principle for empty types.

IsEmpty.elim' definition

{β : Sort*} (h : IsEmpty α) (a : α) : β

Full source

/-- Non-dependent version of `IsEmpty.elim`. Helpful if the elaborator cannot elaborate `h.elim a`
correctly. -/
protected def elim' {β : Sort*} (h : IsEmpty α) (a : α) : β :=
  (h.false a).elim

Vacuous function from an empty type

Informal description

Given a type $\alpha$ that is empty (i.e., has no elements) and an arbitrary type $\beta$, the function maps any element $a$ of $\alpha$ to any element of $\beta$. This is possible because the assumption that $\alpha$ is empty implies that $a$ cannot exist, allowing the function to vacuously satisfy the type requirement.

IsEmpty.prop_iff theorem

{p : Prop} : IsEmpty p ↔ ¬p

Full source

protected theorem prop_iff {p : Prop} : IsEmptyIsEmpty p ↔ ¬p :=
  isEmpty_iff

Empty Proposition iff False

Informal description

For any proposition $p$, the type $p$ is empty if and only if $p$ is false, i.e., $\text{IsEmpty}(p) \leftrightarrow \neg p$.

IsEmpty.forall_iff theorem

{p : α → Prop} : (∀ a, p a) ↔ True

Full source

@[simp]
theorem forall_iff {p : α → Prop} : (∀ a, p a) ↔ True :=
  iff_true_intro isEmptyElim

Universal Quantification over Empty Type is Trivially True

Informal description

For any type $\alpha$ that is empty and any predicate $p$ on $\alpha$, the universal statement "for all $a$ in $\alpha$, $p(a)$ holds" is equivalent to true. In other words, $\forall a \in \alpha, p(a) \leftrightarrow \text{True}$.

IsEmpty.exists_iff theorem

{p : α → Prop} : (∃ a, p a) ↔ False

Full source

@[simp]
theorem exists_iff {p : α → Prop} : (∃ a, p a) ↔ False :=
  iff_false_intro fun ⟨x, _⟩ ↦ IsEmpty.false x

Existence in Empty Type is False

Informal description

For any type $\alpha$ that is empty (i.e., has no elements) and any predicate $p$ on $\alpha$, the statement "there exists an element $a$ in $\alpha$ such that $p(a)$ holds" is equivalent to false. In other words, $\exists a \in \alpha, p(a) \leftrightarrow \text{False}$.

IsEmpty.instSubsingleton instance

: Subsingleton α

Full source

instance (priority := 100) : Subsingleton α :=
  ⟨isEmptyElim⟩

Empty Types are Subsingletons

Informal description

Every empty type is a subsingleton (i.e., has at most one element).

not_nonempty_iff theorem

: ¬Nonempty α ↔ IsEmpty α

Full source

@[simp]
theorem not_nonempty_iff : ¬Nonempty α¬Nonempty α ↔ IsEmpty α :=
  ⟨fun h ↦ ⟨fun x ↦ h ⟨x⟩⟩, fun h1 h2 ↦ h2.elim h1.elim⟩

Equivalence of Non-Emptiness and Emptiness for Types

Informal description

For any type $\alpha$, the statement "$\alpha$ is not nonempty" is equivalent to "$\alpha$ is empty", i.e., $\neg \text{Nonempty}(\alpha) \leftrightarrow \text{IsEmpty}(\alpha)$.

not_isEmpty_iff theorem

: ¬IsEmpty α ↔ Nonempty α

Full source

@[simp]
theorem not_isEmpty_iff : ¬IsEmpty α¬IsEmpty α ↔ Nonempty α :=
  not_iff_comm.mp not_nonempty_iff

Equivalence of Non-Emptiness and Nonemptyness for Types

Informal description

For any type $\alpha$, the statement "$\alpha$ is not empty" is equivalent to "$\alpha$ is nonempty", i.e., $\neg \text{IsEmpty}(\alpha) \leftrightarrow \text{Nonempty}(\alpha)$.

isEmpty_Prop theorem

{p : Prop} : IsEmpty p ↔ ¬p

Full source

@[simp]
theorem isEmpty_Prop {p : Prop} : IsEmptyIsEmpty p ↔ ¬p := by
  simp only [← not_nonempty_iff, nonempty_prop]

Empty Proposition iff False

Informal description

For any proposition $p$, the type $p$ is empty if and only if $p$ is false, i.e., $\text{IsEmpty}(p) \leftrightarrow \neg p$.

isEmpty_pi theorem

{π : α → Sort*} : IsEmpty (∀ a, π a) ↔ ∃ a, IsEmpty (π a)

Full source

@[simp]
theorem isEmpty_pi {π : α → Sort*} : IsEmptyIsEmpty (∀ a, π a) ↔ ∃ a, IsEmpty (π a) := by
  simp only [← not_nonempty_iff, Classical.nonempty_pi, not_forall]

Dependent Function Type is Empty if and only if Some Fiber is Empty

Informal description

For a family of types $\pi : \alpha \to \text{Sort*}$, the type of dependent functions $\forall a, \pi(a)$ is empty if and only if there exists some $a$ for which $\pi(a)$ is empty.

isEmpty_fun theorem

: IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Full source

theorem isEmpty_fun : IsEmptyIsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β := by
  rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

Function Type is Empty iff Domain is Nonempty and Codomain is Empty

Informal description

For any types $\alpha$ and $\beta$, the function type $\alpha \to \beta$ is empty if and only if $\alpha$ is nonempty and $\beta$ is empty.

nonempty_fun theorem

: Nonempty (α → β) ↔ IsEmpty α ∨ Nonempty β

Full source

@[simp]
theorem nonempty_fun : NonemptyNonempty (α → β) ↔ IsEmpty α ∨ Nonempty β :=
  not_iff_not.mp <| by rw [not_or, not_nonempty_iff, not_nonempty_iff, isEmpty_fun, not_isEmpty_iff]

Nonemptiness of Function Type: $\text{Nonempty}(\alpha \to \beta) \leftrightarrow \text{IsEmpty}(\alpha) \lor \text{Nonempty}(\beta)$

Informal description

For any types $\alpha$ and $\beta$, the function type $\alpha \to \beta$ is nonempty if and only if either $\alpha$ is empty or $\beta$ is nonempty.

isEmpty_sigma theorem

{α} {E : α → Type*} : IsEmpty (Sigma E) ↔ ∀ a, IsEmpty (E a)

Full source

@[simp]
theorem isEmpty_sigma {α} {E : α → Type*} : IsEmptyIsEmpty (Sigma E) ↔ ∀ a, IsEmpty (E a) := by
  simp only [← not_nonempty_iff, nonempty_sigma, not_exists]

Emptyness of Dependent Sum Type $\Sigma E$

Informal description

For any type family $E : \alpha \to \text{Type*}$, the dependent sum type $\Sigma E$ is empty if and only if for every element $a : \alpha$, the type $E(a)$ is empty.

isEmpty_psigma theorem

{α} {E : α → Sort*} : IsEmpty (PSigma E) ↔ ∀ a, IsEmpty (E a)

Full source

@[simp]
theorem isEmpty_psigma {α} {E : α → Sort*} : IsEmptyIsEmpty (PSigma E) ↔ ∀ a, IsEmpty (E a) := by
  simp only [← not_nonempty_iff, nonempty_psigma, not_exists]

Dependent Sum Type is Empty if and only if All Fibers are Empty

Informal description

For any type family $E : \alpha \to \text{Sort}^*$, the dependent sum type $\Sigma a:\alpha, E(a)$ is empty if and only if for every $a : \alpha$, the type $E(a)$ is empty.

isEmpty_subtype theorem

(p : α → Prop) : IsEmpty (Subtype p) ↔ ∀ x, ¬p x

Full source

theorem isEmpty_subtype (p : α → Prop) : IsEmptyIsEmpty (Subtype p) ↔ ∀ x, ¬p x := by
  simp only [← not_nonempty_iff, nonempty_subtype, not_exists]

Characterization of Empty Subtypes: $\{x \mid p(x)\} = \emptyset \leftrightarrow \forall x, \neg p(x)$

Informal description

For any predicate $p$ on a type $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ is empty if and only if for every $x \in \alpha$, the proposition $p(x)$ does not hold.

isEmpty_prod theorem

{α β : Type*} : IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Full source

@[simp]
theorem isEmpty_prod {α β : Type*} : IsEmptyIsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

Product Type is Empty iff One Component is Empty

Informal description

For any types $\alpha$ and $\beta$, the product type $\alpha \times \beta$ is empty if and only if at least one of $\alpha$ or $\beta$ is empty.

isEmpty_pprod theorem

: IsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β

Full source

@[simp]
theorem isEmpty_pprod : IsEmptyIsEmpty (PProd α β) ↔ IsEmpty α ∨ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_pprod, not_and_or]

Empty Product Type Condition for `PProd`

Informal description

The product type `PProd α β` is empty if and only if at least one of the types `α` or `β` is empty.

isEmpty_sum theorem

{α β} : IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Full source

@[simp]
theorem isEmpty_sum {α β} : IsEmptyIsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_sum, not_or]

Emptiness of Sum Type $\alpha \oplus \beta$ iff Both $\alpha$ and $\beta$ are Empty

Informal description

For any types $\alpha$ and $\beta$, the sum type $\alpha \oplus \beta$ is empty if and only if both $\alpha$ and $\beta$ are empty.

isEmpty_psum theorem

{α β} : IsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β

Full source

@[simp]
theorem isEmpty_psum {α β} : IsEmptyIsEmpty (α ⊕' β) ↔ IsEmpty α ∧ IsEmpty β := by
  simp only [← not_nonempty_iff, nonempty_psum, not_or]

Emptiness of PSum Type $\alpha \oplus' \beta$ iff Both $\alpha$ and $\beta$ are Empty

Informal description

For any types $\alpha$ and $\beta$, the sum type $\alpha \oplus' \beta$ is empty if and only if both $\alpha$ and $\beta$ are empty.

isEmpty_ulift theorem

{α} : IsEmpty (ULift α) ↔ IsEmpty α

Full source

@[simp]
theorem isEmpty_ulift {α} : IsEmptyIsEmpty (ULift α) ↔ IsEmpty α := by
  simp only [← not_nonempty_iff, nonempty_ulift]

Emptiness of Lifted Type $\text{ULift}\,\alpha$ iff $\alpha$ is Empty

Informal description

For any type $\alpha$, the lifted type $\text{ULift}\,\alpha$ is empty if and only if $\alpha$ is empty.

isEmpty_plift theorem

{α} : IsEmpty (PLift α) ↔ IsEmpty α

Full source

@[simp]
theorem isEmpty_plift {α} : IsEmptyIsEmpty (PLift α) ↔ IsEmpty α := by
  simp only [← not_nonempty_iff, nonempty_plift]

Emptyness of Universe-Lifted Type Equivalence

Informal description

For any type $\alpha$, the type `PLift α` (the universe-lifted version of $\alpha$) is empty if and only if $\alpha$ itself is empty.

wellFounded_of_isEmpty theorem

{α} [IsEmpty α] (r : α → α → Prop) : WellFounded r

Full source

theorem wellFounded_of_isEmpty {α} [IsEmpty α] (r : α → α → Prop) : WellFounded r :=
  ⟨isEmptyElim⟩

Well-foundedness of Relations on Empty Types

Informal description

For any empty type $\alpha$ (i.e., a type with no elements) and any binary relation $r$ on $\alpha$, the relation $r$ is well-founded.

isEmpty_or_nonempty theorem

: IsEmpty α ∨ Nonempty α

Full source

theorem isEmpty_or_nonempty : IsEmptyIsEmpty α ∨ Nonempty α :=
  (em <| IsEmpty α).elim Or.inl <| Or.inrOr.inr ∘ not_isEmpty_iff.mp

Law of Excluded Middle for Type Emptiness

Informal description

For any type $\alpha$, either $\alpha$ is empty or $\alpha$ is nonempty.

not_isEmpty_of_nonempty theorem

[h : Nonempty α] : ¬IsEmpty α

Full source

@[simp]
theorem not_isEmpty_of_nonempty [h : Nonempty α] : ¬IsEmpty α :=
  not_isEmpty_iff.mpr h

Nonempty Types Are Not Empty

Informal description

For any type $\alpha$, if $\alpha$ is nonempty (i.e., there exists an element of type $\alpha$), then $\alpha$ is not empty (i.e., $\neg \text{IsEmpty}(\alpha)$ holds).

Function.extend_of_isEmpty theorem

[IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) : Function.extend f g h = h

Full source

theorem Function.extend_of_isEmpty [IsEmpty α] (f : α → β) (g : α → γ) (h : β → γ) :
    Function.extend f g h = h :=
  funext fun _ ↦ (Function.extend_apply' _ _ _) fun ⟨a, _⟩ ↦ isEmptyElim a

Extension of Functions from Empty Domain Equals Default Function

Informal description

For any type $\alpha$ that is empty, and any functions $f : \alpha \to \beta$, $g : \alpha \to \gamma$, and $h : \beta \to \gamma$, the extension of $g$ along $f$ with default function $h$ is equal to $h$, i.e., $\text{extend}\,f\,g\,h = h$.

leftTotal_empty theorem

[IsEmpty α] : LeftTotal R

Full source

@[simp]
theorem leftTotal_empty [IsEmpty α] : LeftTotal R := by
  simp only [LeftTotal, IsEmpty.forall_iff]

Left Total Relation on Empty Domain

Informal description

If a type $\alpha$ is empty (i.e., `IsEmpty α` holds), then any relation $R$ on $\alpha \times \beta$ is left total. That is, for every $a \in \alpha$, there exists $b \in \beta$ such that $R(a, b)$ holds.

leftTotal_iff_isEmpty_left theorem

[IsEmpty β] : LeftTotal R ↔ IsEmpty α

Full source

theorem leftTotal_iff_isEmpty_left [IsEmpty β] : LeftTotalLeftTotal R ↔ IsEmpty α := by
  simp only [LeftTotal, IsEmpty.exists_iff, isEmpty_iff]

Left Total Relation Characterization with Empty Codomain: $R$ left total $\leftrightarrow$ $\alpha$ empty when $\beta$ empty

Informal description

For any relation $R$ between types $\alpha$ and $\beta$, if $\beta$ is empty, then $R$ is left total if and only if $\alpha$ is empty.

rightTotal_empty theorem

[IsEmpty β] : RightTotal R

Full source

@[simp]
theorem rightTotal_empty [IsEmpty β] : RightTotal R := by
  simp only [RightTotal, IsEmpty.forall_iff]

Right Total Relation on Empty Codomain

Informal description

If the type $\beta$ is empty, then any relation $R$ on $\alpha \times \beta$ is right total.

rightTotal_iff_isEmpty_right theorem

[IsEmpty α] : RightTotal R ↔ IsEmpty β

Full source

theorem rightTotal_iff_isEmpty_right [IsEmpty α] : RightTotalRightTotal R ↔ IsEmpty β := by
  simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff, imp_self]

Right Total Relation Characterization with Empty Domain: $R$ right total $\leftrightarrow$ $\beta$ empty when $\alpha$ empty

Informal description

For any relation $R$ between types $\alpha$ and $\beta$, if $\alpha$ is empty, then $R$ is right total if and only if $\beta$ is empty.

biTotal_empty theorem

[IsEmpty α] [IsEmpty β] : BiTotal R

Full source

@[simp]
theorem biTotal_empty [IsEmpty α] [IsEmpty β] : BiTotal R :=
  ⟨leftTotal_empty R, rightTotal_empty R⟩

Bi-total Relation on Empty Types

Informal description

If the types $\alpha$ and $\beta$ are both empty (i.e., `IsEmpty α` and `IsEmpty β` hold), then any relation $R$ on $\alpha \times \beta$ is bi-total.

biTotal_iff_isEmpty_right theorem

[IsEmpty α] : BiTotal R ↔ IsEmpty β

Full source

theorem biTotal_iff_isEmpty_right [IsEmpty α] : BiTotalBiTotal R ↔ IsEmpty β := by
  simp only [BiTotal, leftTotal_empty, rightTotal_iff_isEmpty_right, true_and]

Bi-total Relation Characterization with Empty Domain: $R$ bi-total $\leftrightarrow$ $\beta$ empty when $\alpha$ empty

Informal description

For any relation $R$ between types $\alpha$ and $\beta$, if $\alpha$ is empty, then $R$ is bi-total if and only if $\beta$ is empty.

biTotal_iff_isEmpty_left theorem

[IsEmpty β] : BiTotal R ↔ IsEmpty α

Full source

theorem biTotal_iff_isEmpty_left [IsEmpty β] : BiTotalBiTotal R ↔ IsEmpty α := by
  simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

Bi-total Relation Characterization with Empty Codomain: $R$ bi-total $\leftrightarrow$ $\alpha$ empty when $\beta$ empty

Informal description

For any relation $R$ between types $\alpha$ and $\beta$, if $\beta$ is empty, then $R$ is bi-total if and only if $\alpha$ is empty.

Main declaration