mathlib documentation

logic.nonempty

Nonempty types #

This file proves a few extra facts about nonempty, which is defined in core Lean.

Main declarations #

@[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) nonempty α
@[simp]
theorem nonempty_Prop {p : Prop} :
theorem not_nonempty_iff_imp_false {α : Sort u_1} :
¬nonempty α α → false
@[simp]
theorem nonempty_sigma {α : Type u_1} {γ : α → Type u_3} :
nonempty (Σ (a : α), γ a) ∃ (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} :
@[simp]
theorem nonempty_pprod {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem nonempty_sum {α : Type u_1} {β : Type u_2} :
@[simp]
theorem nonempty_psum {α : Sort u_1} {β : Sort u_2} :
@[simp]
theorem nonempty_psigma {α : Sort u_1} {β : α → Sort u_2} :
nonempty (psigma β) ∃ (a : α), nonempty (β a)
@[simp]
@[simp]
theorem nonempty_ulift {α : Type u_1} :
@[simp]
theorem nonempty_plift {α : Sort u_1} :
@[simp]
theorem nonempty.forall {α : Sort u_1} {p : nonempty α → Prop} :
(∀ (h : nonempty α), p h) ∀ (a : α), p _
@[simp]
theorem nonempty.exists {α : Sort u_1} {p : nonempty α → Prop} :
(∃ (h : nonempty α), p h) ∃ (a : α), p _
theorem classical.nonempty_pi {α : Sort u_1} {β : α → Sort u_2} :
nonempty (Π (a : α), β a) ∀ (a : α), nonempty (β a)
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]
noncomputable def nonempty.some {α : Sort u_1} (h : nonempty α) :
α

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

Equations
@[protected]
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 : α → β) :
nonempty αnonempty β

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 : α → β → γ) :
nonempty αnonempty βnonempty γ
@[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 : inhabited α → p) :
p
@[protected, instance]
def prod.nonempty {α : Type u_1} {β : Type u_2} [h : nonempty α] [h2 : nonempty β] :
nonempty × β)
theorem subsingleton_of_not_nonempty {α : Sort u_1} (h : ¬nonempty α) :
theorem function.surjective.nonempty {α : Type u_1} {β : Type u_2} [h : nonempty β] {f : α → β} (hf : function.surjective f) :