scilib documentation

logic.nonempty

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 #

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
source
@[protected, reducible]
noncomputable def nonempty.some {α : Sort u_1} (h : nonempty α) :
α

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

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

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

Equations
source
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.

source
@[protected]
theorem nonempty.map2 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) :
nonempty α → nonempty β → nonempty γ
source
@[protected]
theorem nonempty.congr {α : Sort u_1} {β : Sort u_2} (f : α → β) (g : β → α) :
nonempty α ↔ nonempty β
source
theorem nonempty.elim_to_inhabited {α : Sort u_1} [h : nonempty α] {p : Prop} (f : inhabited α → p) :
p
source
@[protected, instance]
def prod.nonempty {α : Type u_1} {β : Type u_2} [h : nonempty α] [h2 : nonempty β] :
nonempty (α × β)
source
@[protected, instance]
def pi.nonempty {ι : Sort u_1} {α : ι → Sort u_2} [∀ (i : ι), nonempty (α i)] :
nonempty (Π (i : ι), α i)
source
theorem classical.nonempty_pi {ι : Sort u_1} {α : ι → Sort u_2} :
nonempty (Π (i : ι), α i) ↔ ∀ (i : ι), nonempty (α i)
source
theorem subsingleton_of_not_nonempty {α : Sort u_1} (h : ¬nonempty α) :
subsingleton α
source
theorem function.surjective.nonempty {α : Sort u_1} {β : Sort u_2} [h : nonempty β] {f : α → β} (hf : function.surjective f) :
nonempty α