English
Let s be a Setoid on α and p a predicate on Quotient s. Then (∀ a, p a) if and only if (∀ a ∈ α, p ⟦a⟧). That is, to prove a statement for all quotients it suffices to prove it for all representatives.
Русский
Пусть s — множество эквивалентности на α, и p — предикат на Quotient s. Тогда (∀ a, p a) эквивалентно (∀ a ∈ α, p ⟦a⟧). Это означает, что для доказательства утверждения про все квоты достаточно доказать его для всех представителей.
LaTeX
$$$\\forall q:\\mathrm{Quotient}(s)\\,\\forall p:\\mathrm{Quotient}(s)\\, (p\,q) \\quad \\text{неверно}\\,\\rightleftharpoons\\, \\forall a:\\alpha, p(\\overline{a})$$$
Lean4
theorem «forall» {α : Sort*} {s : Setoid α} {p : Quotient s → Prop} : (∀ a, p a) ↔ ∀ a : α, p ⟦a⟧ :=
⟨fun h _ ↦ h _, fun h a ↦ a.ind h⟩
