Documentation

Mathlib.Logic.Nonempty

Nonempty types #

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

Main declarations #

@[simp]
theorem Nonempty.forall {α : Sort u_3} {p : Nonempty αProp} :
(∀ (h : Nonempty α), p h) ∀ (a : α), p
@[simp]
theorem Nonempty.exists {α : Sort u_3} {p : Nonempty αProp} :
(∃ (h : Nonempty α), p h) ∃ (a : α), p
theorem exists_true_iff_nonempty {α : Sort u_3} :
(∃ (x : α), True) Nonempty α
@[deprecated nonempty_prop]
theorem nonempty_Prop {p : Prop} :

Alias of nonempty_prop.

theorem Nonempty.imp {α : Sort u_3} {p : Prop} :
Nonempty αp αp
@[simp]
theorem nonempty_psigma {α : Sort u_4} {β : αSort u_3} :
Nonempty (PSigma β) ∃ (a : α), Nonempty (β a)
@[simp]
theorem nonempty_subtype {α : Sort u_3} {p : αProp} :
Nonempty (Subtype p) ∃ (a : α), p a
@[simp]
theorem nonempty_pprod {α : Sort u_3} {β : Sort u_4} :
@[simp]
theorem nonempty_psum {α : Sort u_3} {β : Sort u_4} :
@[simp]
theorem nonempty_plift {α : Sort u_3} :
noncomputable def Classical.inhabited_of_nonempty' {α : Sort u_3} [h : Nonempty α] :

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.

Equations
Instances For
    @[reducible, inline]
    noncomputable abbrev Nonempty.some {α : Sort u_3} (h : Nonempty α) :
    α

    Using Classical.choice, extracts a term from a Nonempty type.

    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev Classical.arbitrary (α : Sort u_3) [h : Nonempty α] :
      α

      Using Classical.choice, extracts a term from a Nonempty type.

      Equations
      Instances For
        theorem Nonempty.map {α : Sort u_3} {β : Sort u_4} (f : αβ) :
        Nonempty αNonempty β

        Given f : α → β, if α is nonempty then β is also nonempty. Nonempty cannot be a functor, because Functor is restricted to Type.

        theorem Nonempty.map2 {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : αβγ) :
        Nonempty αNonempty βNonempty γ
        theorem Nonempty.congr {α : Sort u_3} {β : Sort u_4} (f : αβ) (g : βα) :
        theorem Nonempty.elim_to_inhabited {α : Sort u_3} [h : Nonempty α] {p : Prop} (f : Inhabited αp) :
        p
        theorem Classical.nonempty_pi {ι : Sort u_4} {α : ιSort u_3} :
        Nonempty ((i : ι) → α i) ∀ (i : ι), Nonempty (α i)
        theorem Function.Surjective.nonempty {α : Sort u_1} {β : Sort u_2} [h : Nonempty β] {f : αβ} (hf : Function.Surjective f) :
        @[instance 20]
        instance Zero.instNonempty {α : Type u_1} [Zero α] :
        Equations
        • =
        @[instance 20]
        instance One.instNonempty {α : Type u_1} [One α] :
        Equations
        • =
        @[simp]
        theorem nonempty_sigma {α : Type u_1} {γ : αType u_3} :
        Nonempty ((a : α) × γ a) ∃ (a : α), Nonempty (γ a)
        @[simp]
        theorem nonempty_sum {α : Type u_1} {β : Type u_2} :
        @[simp]
        theorem nonempty_prod {α : Type u_1} {β : Type u_2} :
        @[simp]
        theorem nonempty_ulift {α : Type u_1} :