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

Equations

• Classical.choose! h = Classical.choose ⋯

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

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

@[simp]

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

@[simp]

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

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} {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