API for ExistsUnique

Here we review some of the API provided for ExistsUnique in Mathlib, and provide some additional tools. (Some of these might be suitable for upstreaming to Mathlib.)

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.