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.
@[protected, instance]
def has_zero.nonempty {α : Type u_1} [has_zero α] :
@[protected, instance]
def has_one.nonempty {α : Type u_1} [has_one α] :
theorem exists_true_iff_nonempty {α : Sort u_1} :
(∃ (a : α), true)
@[simp]
theorem nonempty_Prop {p : Prop} :
p
theorem not_nonempty_iff_imp_false {α : Sort u_1} :
α → false
@[simp]
theorem nonempty_sigma {α : Type u_1} {γ : α → Type u_3} :
nonempty (Σ (a : α), γ a) ∃ (a : α), nonempty (γ a)
@[simp]
theorem nonempty_psigma {α : Sort u_1} {β : α → Sort u_2} :
nonempty (psigma β) ∃ (a : α), nonempty (β a)
@[simp]
theorem nonempty_subtype {α : Sort u_1} {p : α → Prop} :
nonempty (subtype p) ∃ (a : α), p a
@[simp]
theorem nonempty_prod {α : Type u_1} {β : Type u_2} :
nonempty × β)
@[simp]
theorem nonempty_pprod {α : Sort u_1} {β : Sort u_2} :
nonempty (pprod α β)
@[simp]
theorem nonempty_sum {α : Type u_1} {β : Type u_2} :
nonempty β)
@[simp]
theorem nonempty_psum {α : Sort u_1} {β : Sort u_2} :
nonempty (psum α β)
@[simp]
theorem nonempty_empty  :
@[simp]
theorem nonempty_ulift {α : Type u_1} :
@[simp]
theorem nonempty_plift {α : Sort u_1} :
@[simp]
theorem nonempty.forall {α : Sort u_1} {p : → Prop} :
(∀ (h : nonempty α), p h) ∀ (a : α), p _
@[simp]
theorem nonempty.exists {α : Sort u_1} {p : → Prop} :
(∃ (h : nonempty α), p h) ∃ (a : α), p _
noncomputable def classical.inhabited_of_nonempty' {α : Sort u_1} [h : nonempty α] :

Using classical.choice, lifts a (Prop-valued) nonempty instance to a (Type-valued) inhabited instance. classical.inhabited_of_nonempty already exists, in core/init/classical.lean, but the assumption is not a type class argument, which makes it unsuitable for some applications.

Equations
@[protected, reducible]
noncomputable def nonempty.some {α : Sort u_1} (h : nonempty α) :
α

Using classical.choice, extracts a term from a nonempty type.

Equations
@[protected, reducible]
noncomputable def classical.arbitrary (α : Sort u_1) [h : nonempty α] :
α

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.

@[protected]
theorem nonempty.map2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) :
@[protected]
theorem nonempty.congr {α : Sort u_1} {β : Sort u_2} (f : α → β) (g : β → α) :
theorem nonempty.elim_to_inhabited {α : Sort u_1} [h : nonempty α] {p : Prop} (f : → p) :
p
@[protected, instance]
def prod.nonempty {α : Type u_1} {β : Type u_2} [h : nonempty α] [h2 : nonempty β] :
nonempty × β)
@[protected, instance]
def pi.nonempty {ι : Sort u_1} {α : ι → Sort u_2} [∀ (i : ι), nonempty (α i)] :
nonempty (Π (i : ι), α i)
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 {α : Type u_1} {β : Type u_2} [h : nonempty β] {f : α → β} (hf : function.surjective f) :