Theorems · Definition

Quotient.congrRight

{α : Sort u} → {r r' : Setoid α} → (∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) → Quotient r ≃ Quotient r'

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.

Defined in

Mathlib.Logic.Equiv.Defs

Cited by

2 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Quot.sound