Theorems · Definition

Quotient.congr

{α : Sort u} →
  {β : Sort v} →
    {ra : Setoid α} →
      {rb : Setoid β} → (e : α ≃ β) → (∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) → Quotient ra ≃ Quotient rb

An equivalence e : α ≃ β generates an equivalence between quotient spaces, if ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Defined in

Mathlib.Logic.Equiv.Defs

Cited by

1 results in Mathlib

Foundations

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