mathlib3 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 #

@[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} :
@[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} :
@[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]
@[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 _
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 : inhabited α 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 : ¬nonempty α) :
theorem function.surjective.nonempty {α : Sort u_1} {β : Sort u_2} [h : nonempty β] {f : α β} (hf : function.surjective f) :