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

This implements the axiom of unique choice.

Equations

• h.choose = ⋯.choose

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

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

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

theorem ExistsUnique.choose_eq_choose {α : Sort u_1} {p : α → Prop} (h : ∃! x : α, p x) : Exists.choose h = h.choose

noncomputable def Subsingleton.choose {α : Sort u_1} [Subsingleton α] [hn : Nonempty α] : α

An alternate form of the axiom of unique choice.

Equations

• Subsingleton.choose = hn.some

theorem Subsingleton.choose_spec {α : Sort u_1} [hs : Subsingleton α] [Nonempty α] (x : α) : x = choose

theorem ExistsUnique.iff_subsingleton_nonempty {α : Sort u_1} {p : α → Prop} : (∃! x : α, p x) ↔ Subsingleton { x : α // p x } ∧ Nonempty { x : α // p x }

The equivalence between ExistsUnique and Subsingleton/Nonempty does not require choice.