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.instNonempty {α : Type u_2} [Zero α] : Nonempty α

Equations

• ⋯ = ⋯

instance One.instNonempty {α : Type u_2} [One α] : Nonempty α

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} : Nonempty p ↔ p

theorem Nonempty.imp {α : Sort u_2} {p : Prop} : Nonempty α → p ↔ α → p

theorem not_nonempty_iff_imp_false {α : Sort u_2} : ¬Nonempty α ↔ α → False

@[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} : Nonempty (α × β) ↔ Nonempty α ∧ Nonempty β

@[simp]

theorem nonempty_pprod {α : Sort u_2} {β : Sort u_3} : Nonempty (PProd α β) ↔ Nonempty α ∧ Nonempty β

@[simp]

theorem nonempty_sum {α : Type u_3} {β : Type u_2} : Nonempty (α ⊕ β) ↔ Nonempty α ∨ Nonempty β

@[simp]

theorem nonempty_psum {α : Sort u_2} {β : Sort u_3} : Nonempty (α ⊕' β) ↔ Nonempty α ∨ Nonempty β

@[simp]

theorem nonempty_ulift {α : Type u_2} : Nonempty (ULift.{u_3, u_2} α) ↔ Nonempty α

@[simp]

theorem nonempty_plift {α : Sort u_2} : Nonempty (PLift α) ↔ Nonempty α

noncomputable def Classical.inhabited_of_nonempty' {α : Sort u_2} [h : Nonempty α] : Inhabited α

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 := Classical.choice h }

@[reducible]

noncomputable def Nonempty.some {α : Sort u_2} (h : Nonempty α) : α

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

Equations

• Nonempty.some h = Classical.choice h

@[reducible]

noncomputable def Classical.arbitrary (α : Sort u_2) [h : Nonempty α] : α

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

Equations

• Classical.arbitrary α = Classical.choice h

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 : β → α) : Nonempty α ↔ Nonempty β

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 subsingleton_of_not_nonempty {α : Sort u_2} (h : ¬Nonempty α) : Subsingleton α

theorem Function.Surjective.nonempty {α : Sort u_3} {β : Sort u_2} [h : Nonempty β] {f : α → β} (hf : Function.Surjective f) : Nonempty α