Documentation

Mathlib.Logic.Nonempty

Nonempty types #

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

Main declarations #

instance Zero.instNonempty {α : Type u_2} [Zero α] :
Equations
  • =
instance One.instNonempty {α : Type u_2} [One α] :
Equations
  • =
@[simp]
theorem Nonempty.forall {α : Sort u_2} {p : Nonempty αProp} :
(∀ (h : Nonempty α), p h) ∀ (a : α), p
@[simp]
theorem Nonempty.exists {α : Sort u_2} {p : Nonempty αProp} :
(∃ (h : Nonempty α), p h) ∃ (a : α), p
theorem exists_true_iff_nonempty {α : Sort u_2} :
(∃ (x : α), True) Nonempty α
@[simp]
theorem nonempty_Prop {p : Prop} :
theorem Nonempty.imp {α : Sort u_2} {p : Prop} :
Nonempty αp αp
@[simp]
theorem nonempty_sigma {α : Type u_2} {γ : αType u_1} :
Nonempty ((a : α) × γ a) ∃ (a : α), Nonempty (γ a)
@[simp]
theorem nonempty_psigma {α : Sort u_3} {β : αSort u_2} :
Nonempty (PSigma β) ∃ (a : α), Nonempty (β a)
@[simp]
theorem nonempty_subtype {α : Sort u_2} {p : αProp} :
Nonempty (Subtype p) ∃ (a : α), p a
@[simp]
theorem nonempty_prod {α : Type u_3} {β : Type u_2} :
@[simp]
theorem nonempty_pprod {α : Sort u_2} {β : Sort u_3} :
@[simp]
theorem nonempty_sum {α : Type u_3} {β : Type u_2} :
@[simp]
theorem nonempty_psum {α : Sort u_2} {β : Sort u_3} :
@[simp]
@[simp]
theorem nonempty_plift {α : Sort u_2} :
noncomputable def Classical.inhabited_of_nonempty' {α : Sort u_2} [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]
    noncomputable def Nonempty.some {α : Sort u_2} (h : Nonempty α) :
    α

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

    Equations
    Instances For
      @[reducible]
      noncomputable def Classical.arbitrary (α : Sort u_2) [h : Nonempty α] :
      α

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

      Equations
      Instances For
        theorem Nonempty.map {α : Sort u_2} {β : Sort u_3} (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_2} {β : Sort u_3} {γ : Sort u_4} (f : αβγ) :
        Nonempty αNonempty βNonempty γ
        theorem Nonempty.congr {α : Sort u_2} {β : Sort u_3} (f : αβ) (g : βα) :
        theorem Nonempty.elim_to_inhabited {α : Sort u_2} [h : Nonempty α] {p : Prop} (f : Inhabited αp) :
        p
        instance Prod.instNonempty {α : Type u_2} {β : Type u_3} [h : Nonempty α] [h2 : Nonempty β] :
        Nonempty (α × β)
        Equations
        • =
        instance Pi.instNonempty {ι : Sort u_2} {α : ιSort u_3} [∀ (i : ι), Nonempty (α i)] :
        Nonempty ((i : ι) → α i)
        Equations
        • =
        theorem Classical.nonempty_pi {ι : Sort u_3} {α : ιSort u_2} :
        Nonempty ((i : ι) → α i) ∀ (i : ι), Nonempty (α i)
        theorem Function.Surjective.nonempty {α : Sort u_3} {β : Sort u_2} [h : Nonempty β] {f : αβ} (hf : Function.Surjective f) :