English
There is a congruence between quotient spaces when the underlying relations are related by an equivalence.
Русский
Существует конгруэнция между пространства́ми частичных классов, если базовые отношения связаны эквивалентностью.
LaTeX
$$$ \forall {r r' : Setoid α}, (\forall a_1 a_2, r a_1 a_2 \leftrightarrow r' a_1 a_2) \rightarrow Quotient r \simeq Quotient r' $$$
Lean4
/-- Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with `eq`, but then computational proofs get stuck. -/
protected def congrRight {r r' : Setoid α} (eq : ∀ a₁ a₂, r a₁ a₂ ↔ r' a₁ a₂) : Quotient r ≃ Quotient r' :=
Quot.congrRight eq
