Documentation

Foundation.Vorspiel.ExistsUnique

noncomputable def Classical.choose! {α : Sort u_1} {p : αProp} (h : ∃! x : α, p x) :
α
Equations
Instances For
    theorem Classical.choose!_spec {α : Sort u_1} {p : αProp} (h : ∃! x : α, p x) :
    theorem Classical.choose_uniq {α : Sort u_1} {p : αProp} (h : ∃! x : α, p x) {x : α} (hx : p x) :
    theorem Classical.choose!_eq_iff {α : Sort u_1} {p : αProp} (h : ∃! x : α, p x) {x : α} :