English
Two setoid structures r1 and r2 on α are equal iff all their equivalence classes are equal; equivalently, r1 = r2 iff for every a, the class { y : α : r1 a y } equals { y : α : r2 a y }.
Русский
Две структуры эквивалентности на α равны тогда и только тогда, когда их эквивалентные классы совпадают; то есть r1 = r2 тогда и только тогда, когда для каждого a множества { y : α : r1(a,y) } совпадает с { y : α : r2(a,y) }.
LaTeX
$$$(r_1 = r_2) \\iff \\forall a, \\{ y : α \\mid r_1(a,y) \\} = \\{ y : α \\mid r_2(a,y) \\}.$$$
Lean4
/-- Two equivalence relations are equal iff all their equivalence classes are equal. -/
theorem eq_iff_classes_eq {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ ∀ x, {y | r₁ x y} = {y | r₂ x y} :=
⟨fun h _x => h ▸ rfl, fun h => ext fun x => Set.ext_iff.1 <| h x⟩
