# Documentation

Mathlib.Logic.Nonempty

# 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.
instance Zero.nonempty {α : Type u_1} [inst : Zero α] :
Equations
instance One.nonempty {α : Type u_1} [inst : One α] :
Equations
theorem exists_true_iff_nonempty {α : Sort u_1} :
(x, True)
@[simp]
theorem nonempty_Prop {p : Prop} :
p
@[simp]
theorem nonempty_sigma {α : Type u_2} {γ : αType u_1} :
Nonempty ((a : α) × γ a) a, Nonempty (γ a)
@[simp]
theorem nonempty_psigma {α : Sort u_1} {β : αSort u_2} :
Nonempty () a, Nonempty (β a)
@[simp]
theorem nonempty_subtype {α : Sort u_1} {p : αProp} :
Nonempty () a, p a
@[simp]
theorem nonempty_prod {α : Type u_2} {β : Type u_1} :
Nonempty (α × β)
@[simp]
theorem nonempty_pprod {α : Sort u_1} {β : Sort u_2} :
Nonempty (PProd α β)
@[simp]
theorem nonempty_sum {α : Type u_2} {β : Type u_1} :
Nonempty (α β)
@[simp]
theorem nonempty_psum {α : Sort u_1} {β : Sort u_2} :
Nonempty (α ⊕' β)
@[simp]
theorem nonempty_ulift {α : Type u_1} :
@[simp]
theorem nonempty_plift {α : Sort u_1} :
@[simp]
theorem Nonempty.forall {α : Sort u_1} {p : Prop} :
((h : ) → p h) (a : α) → p (_ : )
@[simp]
theorem Nonempty.exists {α : Sort u_1} {p : Prop} :
(h, p h) a, p (_ : )
noncomputable def Classical.inhabited_of_nonempty' {α : Sort u_1} [h : ] :

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
• Classical.inhabited_of_nonempty' = { default := }
noncomputable def Nonempty.some {α : Sort u_1} (h : ) :
α

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

Equations
noncomputable def Classical.arbitrary (α : Sort u_1) [h : ] :
α

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

Equations
theorem Nonempty.map {α : Sort u_1} {β : Sort u_2} (f : αβ) :

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_1} {β : Sort u_2} {γ : Sort u_3} (f : αβγ) :
theorem Nonempty.congr {α : Sort u_1} {β : Sort u_2} (f : αβ) (g : βα) :
theorem Nonempty.elim_to_inhabited {α : Sort u_1} [h : ] {p : Prop} (f : p) :
p
instance Prod.Nonempty {α : Type u_1} {β : Type u_2} [h : ] [h2 : ] :
Nonempty (α × β)
Equations
instance Pi.Nonempty {ι : Sort u_1} {α : ιSort u_2} [inst : ∀ (i : ι), Nonempty (α i)] :
Nonempty ((i : ι) → α i)
Equations
theorem Classical.nonempty_pi {ι : Sort u_1} {α : ιSort u_2} :
Nonempty ((i : ι) → α i) ∀ (i : ι), Nonempty (α i)
theorem subsingleton_of_not_nonempty {α : Sort u_1} (h : ) :
theorem Function.Surjective.nonempty {α : Sort u_2} {β : Sort u_1} [h : ] {f : αβ} (hf : ) :