noncomputable def Classical.choose! {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) : α

Equations

• Classical.choose! h = Classical.choose ⋯

theorem Classical.choose!_spec {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) : p (Classical.choose! h)

theorem Classical.choose_uniq {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) {x : α} (hx : p x) : x = Classical.choose! h

theorem Classical.choose!_eq_iff {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) {x : α} : x = Classical.choose! h ↔ p x