English
Let p be a predicate on Quotient s. Then (∃ a, p a) if and only if ∃ a : α, p ⟦a⟧; i.e., existence can be witnessed by a representative.
Русский
Пусть p — предикат на Quotient s. Тогда (∃ a, p a) эквивалентно ∃ a : α, p ⟦a⟧; т.е. существование может быть засвидетельствовано представителем.
LaTeX
$$$\\Exists a:\\mathrm{Quotient}(s).\\; p\,a \\;\\Leftrightarrow\\; \\Exists a:\\alpha,\\, p(\\overline{a})$$$
Lean4
theorem «exists» {α : Sort*} {s : Setoid α} {p : Quotient s → Prop} : (∃ a, p a) ↔ ∃ a : α, p ⟦a⟧ :=
⟨fun ⟨q, hq⟩ ↦ q.ind (motive := (p · → _)) .intro hq, fun ⟨a, ha⟩ ↦ ⟨⟦a⟧, ha⟩⟩
