doc-next-gen

Mathlib.Logic.Nonempty

Module docstring

{"# Nonempty types

This file proves a few extra facts about Nonempty, which is defined in core Lean.

Main declarations

  • Nonempty.some: Extracts a witness of nonemptiness using choice. Takes Nonempty α explicitly.
  • Classical.arbitrary: Extracts a witness of nonemptiness using choice. Takes Nonempty α as an instance. "}
Nonempty.forall theorem
{α} {p : Nonempty α → Prop} : (∀ h : Nonempty α, p h) ↔ ∀ a, p ⟨a⟩
Full source 
@[simp]
theorem Nonempty.forall {α} {p : Nonempty α → Prop} : (∀ h : Nonempty α, p h) ↔ ∀ a, p ⟨a⟩ :=
  Iff.intro (fun h _ ↦ h _) fun h ⟨a⟩ ↦ h a
Universal Quantification over Nonempty Proofs vs Elements
Informal description
For any type `α` and any predicate `p` on `Nonempty α`, the following are equivalent: 1. For all proofs `h` that `α` is nonempty, `p h` holds. 2. For every element `a : α`, the predicate `p` holds for the trivial proof `⟨a⟩` of nonemptiness. In other words, a universal quantification over all proofs of `Nonempty α` is equivalent to a universal quantification over all elements of `α` (when applied to the trivial proof).
Nonempty.exists theorem
{α} {p : Nonempty α → Prop} : (∃ h : Nonempty α, p h) ↔ ∃ a, p ⟨a⟩
Full source 
@[simp]
theorem Nonempty.exists {α} {p : Nonempty α → Prop} : (∃ h : Nonempty α, p h) ↔ ∃ a, p ⟨a⟩ :=
  Iff.intro (fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦ ⟨⟨a⟩, h⟩
Existence in Nonempty Types
Informal description
For any type $\alpha$ and any predicate $p$ on `Nonempty α`, there exists a proof `h` that $\alpha$ is nonempty such that $p(h)$ holds if and only if there exists an element $a : \alpha$ such that $p(\langle a \rangle)$ holds, where $\langle a \rangle$ is the canonical proof that $\alpha$ is nonempty given by $a$.
exists_const_iff theorem
{α : Sort*} {P : Prop} : (∃ _ : α, P) ↔ Nonempty α ∧ P
Full source 
@[simp low]
theorem exists_const_iff {α : Sort*} {P : Prop} : (∃ _ : α, P) ↔ Nonempty α ∧ P :=
  Iff.intro (fun ⟨a, h⟩ ↦ ⟨⟨a⟩, h⟩) fun ⟨⟨a⟩, h⟩ ↦ ⟨a, h⟩
Existence of Constant Proposition Equivalent to Nonemptiness and Proposition
Informal description
For any type $\alpha$ and any proposition $P$, the statement "there exists an element of $\alpha$ such that $P$ holds" is equivalent to "$\alpha$ is nonempty and $P$ holds".
exists_true_iff_nonempty theorem
{α : Sort*} : (∃ _ : α, True) ↔ Nonempty α
Full source 
theorem exists_true_iff_nonempty {α : Sort*} : (∃ _ : α, True) ↔ Nonempty α :=
  Iff.intro (fun ⟨a, _⟩ ↦ ⟨a⟩) fun ⟨a⟩ ↦ ⟨a, trivial⟩
Existence of Trivial Element Characterizes Nonempty Types
Informal description
For any type $\alpha$, the statement "there exists an element of $\alpha$ such that `True`" is equivalent to $\alpha$ being nonempty. In other words, $(\exists x : \alpha, \text{True}) \leftrightarrow \text{Nonempty}(\alpha)$.
Nonempty.imp theorem
{α} {p : Prop} : (Nonempty α → p) ↔ (α → p)
Full source 
theorem Nonempty.imp {α} {p : Prop} : (Nonempty α → p) ↔ (α → p) :=
  Nonempty.forall
Implication from Nonemptiness vs Universal Quantification over Elements
Informal description
For any type $\alpha$ and any proposition $p$, the implication "if $\alpha$ is nonempty then $p$ holds" is equivalent to "for every element $a : \alpha$, $p$ holds".
not_nonempty_iff_imp_false theorem
{α : Sort*} : ¬Nonempty α ↔ α → False
Full source 
theorem not_nonempty_iff_imp_false {α : Sort*} : ¬Nonempty α¬Nonempty α ↔ α → False :=
  Nonempty.imp
Empty Type Characterization: $\neg \text{Nonempty}(\alpha) \leftrightarrow (\alpha \to \text{False})$
Informal description
For any type $\alpha$, the statement "$\alpha$ is empty" is equivalent to "every element of $\alpha$ implies false". In other words, $\neg \text{Nonempty}(\alpha) \leftrightarrow (\forall x : \alpha, \text{False})$.
nonempty_psigma theorem
{α} {β : α → Sort*} : Nonempty (PSigma β) ↔ ∃ a : α, Nonempty (β a)
Full source 
@[simp]
theorem nonempty_psigma {α} {β : α → Sort*} : NonemptyNonempty (PSigma β) ↔ ∃ a : α, Nonempty (β a) :=
  Iff.intro (fun ⟨⟨a, c⟩⟩ ↦ ⟨a, ⟨c⟩⟩) fun ⟨a, ⟨c⟩⟩ ↦ ⟨⟨a, c⟩⟩
Nonemptiness of Dependent Sum Type ↔ Existence of Nonempty Fiber
Informal description
For any type `α` and a family of types `β : α → Sort*`, the dependent sum type `PSigma β` is nonempty if and only if there exists an element `a : α` such that the type `β a` is nonempty.
nonempty_subtype theorem
{α} {p : α → Prop} : Nonempty (Subtype p) ↔ ∃ a : α, p a
Full source 
@[simp]
theorem nonempty_subtype {α} {p : α → Prop} : NonemptyNonempty (Subtype p) ↔ ∃ a : α, p a :=
  Iff.intro (fun ⟨⟨a, h⟩⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦ ⟨⟨a, h⟩⟩
Nonempty Subtype Characterization
Informal description
For any type $\alpha$ and predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ is nonempty if and only if there exists an element $a \in \alpha$ such that $p(a)$ holds.
nonempty_pprod theorem
{α β} : Nonempty (PProd α β) ↔ Nonempty α ∧ Nonempty β
Full source 
@[simp]
theorem nonempty_pprod {α β} : NonemptyNonempty (PProd α β) ↔ Nonempty α ∧ Nonempty β :=
  Iff.intro (fun ⟨⟨a, b⟩⟩ ↦ ⟨⟨a⟩, ⟨b⟩⟩) fun ⟨⟨a⟩, ⟨b⟩⟩ ↦ ⟨⟨a, b⟩⟩
Nonempty Product Type Characterization
Informal description
For any types $\alpha$ and $\beta$, the product type $PProd\,\alpha\,\beta$ is nonempty if and only if both $\alpha$ and $\beta$ are nonempty.
nonempty_psum theorem
{α β} : Nonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β
Full source 
@[simp]
theorem nonempty_psum {α β} : NonemptyNonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β :=
  Iff.intro
    (fun ⟨h⟩ ↦
      match h with
      | PSum.inl a => Or.inl ⟨a⟩
      | PSum.inr b => Or.inr ⟨b⟩)
    fun h ↦
    match h with
    | Or.inl ⟨a⟩ => ⟨PSum.inl a⟩
    | Or.inr ⟨b⟩ => ⟨PSum.inr b⟩
Nonempty Sum Type Characterization: $\alpha \oplus' \beta$ nonempty iff $\alpha$ or $\beta$ nonempty
Informal description
For any types $\alpha$ and $\beta$, the sum type $\alpha \oplus' \beta$ is nonempty if and only if at least one of $\alpha$ or $\beta$ is nonempty.
Classical.inhabited_of_nonempty' definition
{α} [h : Nonempty α] : Inhabited α
Full source 
/-- Using `Classical.choice`, lifts a (`Prop`-valued) `Nonempty` instance to a (`Type`-valued)
`Inhabited` instance. `Classical.inhabited_of_nonempty` already exists, in `Init/Classical.lean`,
but the assumption is not a type class argument, which makes it unsuitable for some applications. -/
noncomputable def Classical.inhabited_of_nonempty' {α} [h : Nonempty α] : Inhabited α :=
  ⟨Classical.choice h⟩
Inhabited instance from nonempty type
Informal description
Given a nonempty type $\alpha$, this definition constructs an instance of `Inhabited α` by selecting an arbitrary element of $\alpha$ using the axiom of choice.
Nonempty.some abbrev
{α} (h : Nonempty α) : α
Full source 
/-- Using `Classical.choice`, extracts a term from a `Nonempty` type. -/
protected noncomputable abbrev Nonempty.some {α} (h : Nonempty α) : α :=
  Classical.choice h
Witness Extraction from Nonempty Type
Informal description
Given a nonempty type $\alpha$ (i.e., `Nonempty α` holds), the function `Nonempty.some` extracts a witness element of type $\alpha$ using the axiom of choice.
Classical.arbitrary abbrev
(α) [h : Nonempty α] : α
Full source 
/-- Using `Classical.choice`, extracts a term from a `Nonempty` type. -/
protected noncomputable abbrev Classical.arbitrary (α) [h : Nonempty α] : α :=
  Classical.choice h
Arbitrary Element Selection via Axiom of Choice
Informal description
Given a nonempty type $\alpha$, the function `Classical.arbitrary` selects an arbitrary element of $\alpha$ using the axiom of choice.
Nonempty.map theorem
{α β} (f : α → β) : Nonempty α → Nonempty β
Full source 
/-- Given `f : α → β`, if `α` is nonempty then `β` is also nonempty.
`Nonempty` cannot be a `functor`, because `Functor` is restricted to `Type`. -/
theorem Nonempty.map {α β} (f : α → β) : Nonempty α → Nonempty β
  | ⟨h⟩ => ⟨f h⟩
Nonempty Preservation under Function Mapping
Informal description
For any function $f : \alpha \to \beta$, if the type $\alpha$ is nonempty, then the type $\beta$ is also nonempty.
Nonempty.map2 theorem
{α β γ : Sort*} (f : α → β → γ) : Nonempty α → Nonempty β → Nonempty γ
Full source 
protected theorem Nonempty.map2 {α β γ : Sort*} (f : α → β → γ) :
    Nonempty α → Nonempty β → Nonempty γ
  | ⟨x⟩, ⟨y⟩ => ⟨f x y⟩
Nonempty Preservation under Binary Function Application
Informal description
For any types $\alpha$, $\beta$, and $\gamma$, and any function $f : \alpha \to \beta \to \gamma$, if $\alpha$ and $\beta$ are nonempty, then $\gamma$ is also nonempty.
Nonempty.congr theorem
{α β} (f : α → β) (g : β → α) : Nonempty α ↔ Nonempty β
Full source 
protected theorem Nonempty.congr {α β} (f : α → β) (g : β → α) : NonemptyNonempty α ↔ Nonempty β :=
  ⟨Nonempty.map f, Nonempty.map g⟩
Nonemptiness Equivalence via Mutual Function Mapping
Informal description
For any types $\alpha$ and $\beta$, and any functions $f : \alpha \to \beta$ and $g : \beta \to \alpha$, the type $\alpha$ is nonempty if and only if the type $\beta$ is nonempty.
Nonempty.elim_to_inhabited theorem
{α : Sort*} [h : Nonempty α] {p : Prop} (f : Inhabited α → p) : p
Full source 
theorem Nonempty.elim_to_inhabited {α : Sort*} [h : Nonempty α] {p : Prop} (f : Inhabited α → p) :
    p :=
  h.elim <| f ∘ Inhabited.mk
Elimination from Nonempty to Inhabited Implies Proposition
Informal description
For any type `α` that is nonempty (i.e., `Nonempty α` holds), and for any proposition `p`, if there exists a function `f` that maps an inhabited instance of `α` to `p`, then `p` holds.
Classical.nonempty_pi theorem
{ι} {α : ι → Sort*} : Nonempty (∀ i, α i) ↔ ∀ i, Nonempty (α i)
Full source 
theorem Classical.nonempty_pi {ι} {α : ι → Sort*} : NonemptyNonempty (∀ i, α i) ↔ ∀ i, Nonempty (α i) :=
  ⟨fun ⟨f⟩ a ↦ ⟨f a⟩, @Pi.instNonempty _ _⟩
Nonemptiness of Dependent Function Space vs. Nonemptiness of Each Component
Informal description
For any family of types $\alpha_i$ indexed by $i \in \iota$, the type of dependent functions $\forall i, \alpha_i$ is nonempty if and only if each $\alpha_i$ is nonempty.
Function.Surjective.nonempty theorem
[h : Nonempty β] {f : α → β} (hf : Function.Surjective f) : Nonempty α
Full source 
theorem Function.Surjective.nonempty [h : Nonempty β] {f : α → β} (hf : Function.Surjective f) :
    Nonempty α :=
  let ⟨y⟩ := h
  let ⟨x, _⟩ := hf y
  ⟨x⟩
Nonemptiness of Domain via Surjective Function
Informal description
If $\beta$ is nonempty and there exists a surjective function $f : \alpha \to \beta$, then $\alpha$ is nonempty.
nonempty_sigma theorem
: Nonempty (Σ a : α, γ a) ↔ ∃ a : α, Nonempty (γ a)
Full source 
@[simp]
theorem nonempty_sigma : NonemptyNonempty (Σa : α, γ a) ↔ ∃ a : α, Nonempty (γ a) :=
  Iff.intro (fun ⟨⟨a, c⟩⟩ ↦ ⟨a, ⟨c⟩⟩) fun ⟨a, ⟨c⟩⟩ ↦ ⟨⟨a, c⟩⟩
Nonemptiness of Dependent Sum Type $\Sigma (a : \alpha), \gamma(a)$
Informal description
The dependent sum type $\Sigma (a : \alpha), \gamma(a)$ is nonempty if and only if there exists an element $a : \alpha$ such that the type $\gamma(a)$ is nonempty.
nonempty_sum theorem
: Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β
Full source 
@[simp]
theorem nonempty_sum : NonemptyNonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β :=
  Iff.intro
    (fun ⟨h⟩ ↦
      match h with
      | Sum.inl a => Or.inl ⟨a⟩
      | Sum.inr b => Or.inr ⟨b⟩)
    fun h ↦
    match h with
    | Or.inl ⟨a⟩ => ⟨Sum.inl a⟩
    | Or.inr ⟨b⟩ => ⟨Sum.inr b⟩
Nonemptiness of Sum Type $\alpha \oplus \beta$
Informal description
The sum type $\alpha \oplus \beta$ is nonempty if and only if either $\alpha$ is nonempty or $\beta$ is nonempty.