Equations
Instances For
theorem
Classical.choose!_spec
{α : Sort u_1}
{p : α → Prop}
(h : ∃! x : α, p x)
:
p (Classical.choose! h)
theorem
Classical.choose_uniq
{α : Sort u_1}
{p : α → Prop}
(h : ∃! x : α, p x)
{x : α}
(hx : p x)
:
x = Classical.choose! h
theorem
Classical.choose!_eq_iff
{α : Sort u_1}
{p : α → Prop}
(h : ∃! x : α, p x)
{x : α}
:
x = Classical.choose! h ↔ p x