Nonempty types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[protected, instance]

def has_zero.nonempty {α : Type u_1} [has_zero α] :

nonempty α

source

@[protected, instance]

def has_one.nonempty {α : Type u_1} [has_one α] :

nonempty α

source

theorem exists_true_iff_nonempty {α : Sort u_1} :

(∃ (a : α), true) ↔ nonempty α

source

@[simp]

theorem nonempty_Prop {p : Prop} :

nonempty p ↔ p

source

theorem not_nonempty_iff_imp_false {α : Sort u_1} :

¬nonempty α ↔ α → false

source

@[simp]

theorem nonempty_sigma {α : Type u_1} {γ : α → Type u_3} :

nonempty (Σ (a : α), γ a) ↔ ∃ (a : α), nonempty (γ a)

source

@[simp]

theorem nonempty_psigma {α : Sort u_1} {β : α → Sort u_2} :

nonempty (psigma β) ↔ ∃ (a : α), nonempty (β a)

source

@[simp]

theorem nonempty_subtype {α : Sort u_1} {p : α → Prop} :

nonempty (subtype p) ↔ ∃ (a : α), p a

source

@[simp]

theorem nonempty_prod {α : Type u_1} {β : Type u_2} :

nonempty (α × β) ↔ nonempty α ∧ nonempty β

source

@[simp]

theorem nonempty_pprod {α : Sort u_1} {β : Sort u_2} :

nonempty (pprod α β) ↔ nonempty α ∧ nonempty β

source

@[simp]

theorem nonempty_sum {α : Type u_1} {β : Type u_2} :

nonempty (α ⊕ β) ↔ nonempty α ∨ nonempty β

source

@[simp]

theorem nonempty_psum {α : Sort u_1} {β : Sort u_2} :

nonempty (psum α β) ↔ nonempty α ∨ nonempty β

source

@[simp]

theorem nonempty_empty :

¬nonempty empty

source

@[simp]

theorem nonempty_ulift {α : Type u_1} :

nonempty (ulift α) ↔ nonempty α

source

@[simp]

theorem nonempty_plift {α : Sort u_1} :

nonempty (plift α) ↔ nonempty α

source

@[simp]

theorem nonempty.forall {α : Sort u_1} {p : nonempty α → Prop} :

(∀ (h : nonempty α), p h) ↔ ∀ (a : α), p _

source

@[simp]

theorem nonempty.exists {α : Sort u_1} {p : nonempty α → Prop} :

(∃ (h : nonempty α), p h) ↔ ∃ (a : α), p _

source

noncomputable def classical.inhabited_of_nonempty' {α : Sort u_1} [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 core/init/classical.lean, but the assumption is not a type class argument, which makes it unsuitable for some applications.

Equations