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 : α) : α

Equations

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

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

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

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

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