# 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.
@[simp]
theorem Nonempty.forall {α : Sort u_3} {p : Prop} :
(∀ (h : ), p h) ∀ (a : α), p
@[simp]
theorem Nonempty.exists {α : Sort u_3} {p : Prop} :
(∃ (h : ), p h) ∃ (a : α), p
theorem exists_true_iff_nonempty {α : Sort u_3} :
(∃ (x : α), True)
@[simp]
theorem nonempty_Prop {p : Prop} :
p
theorem Nonempty.imp {α : Sort u_3} {p : Prop} :
p αp
theorem not_nonempty_iff_imp_false {α : Sort u_3} :
αFalse
@[simp]
theorem nonempty_psigma {α : Sort u_4} {β : αSort u_3} :
Nonempty () ∃ (a : α), Nonempty (β a)
@[simp]
theorem nonempty_subtype {α : Sort u_3} {p : αProp} :
Nonempty () ∃ (a : α), p a
@[simp]
theorem nonempty_pprod {α : Sort u_3} {β : Sort u_4} :
Nonempty (PProd α β)
@[simp]
theorem nonempty_psum {α : Sort u_3} {β : Sort u_4} :
Nonempty (α ⊕' β)
@[simp]
theorem nonempty_plift {α : Sort u_3} :
noncomputable def Classical.inhabited_of_nonempty' {α : Sort u_3} [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 := }
Instances For
@[reducible, inline]
noncomputable abbrev Nonempty.some {α : Sort u_3} (h : ) :
α

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

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

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

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