ExistsUnique

theorem Classical.exitsUnique_extend {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default x : α) : ∃! y : α, (p x → r x y) ∧ (¬p x → y = default)

noncomputable def Classical.extendedChoose! {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default x : α) : α

Imported declaration from the Incompleteness formalization.

Equations

• Classical.extendedChoose! h default x = Classical.choose ⋯

theorem Classical.extendedchoose!_spec {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hx : p x) : r x (extendedChoose! h default x)

theorem Classical.extendedchoose!_spec_not {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hx : ¬p x) : extendedChoose! h default x = default

theorem Classical.extendedChoose!_uniq {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x y : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hpx : p x) (hrx : r x y) : y = extendedChoose! h default x

theorem Classical.extendedChoose!_eq_iff {α : Sort u_1} {p : α → Prop} {r : α → α → Prop} {x y : α} (h : ∀ (x : α), p x → ∃! y : α, r x y) (default : α) (hpx : p x) : y = extendedChoose! h default x ↔ r x y