ExistsUnique

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

Imported declaration from the Incompleteness formalization.

Equations

• Classical.choose! h = Classical.choose ⋯

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

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

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