English
In a quotient by a Setoid r, two representatives x and y satisfy Quot.mk r x = Quot.mk r y if and only if x is related to y under the generated equivalence EqvGen r.
Русский
В квоте по отношению эквивалентности r равенство представлений x и y эквивалентно тому, что x и y связаны сгенерированной эквивалентностью EqvGen r.
LaTeX
$$$\\Quot{r}{x} = \\Quot{r}{y} \\;\\iff\\; \\mathrm{EqvGen}(r)(x,y)$$$
Lean4
theorem eq {α : Type*} {r : α → α → Prop} {x y : α} : Quot.mk r x = Quot.mk r y ↔ Relation.EqvGen r x y :=
⟨Quot.eqvGen_exact, Quot.eqvGen_sound⟩
