classes_inj — Mathlib

English

Two setoid structures r1 and r2 on α are equal iff their sets of equivalence classes are equal.

Русский

Две структуры эквивалентности равны тогда и только тогда, когда их множества эквивалентных классов совпадают.

LaTeX

$$$(r_1 = r_2) \\iff (r_1.classes = r_2.classes).$$$

Lean4

/-- Two equivalence relations are equal iff their equivalence classes are equal. -/
theorem classes_inj {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ r₁.classes = r₂.classes :=
  ⟨fun h => h ▸ rfl, fun h => ext fun a b => by simp only [rel_iff_exists_classes, h]⟩

Похожие утверждения