congr — Mathlib

English

An equivalence e: α ≃ β with eq relating ra and rb induces an equivalence between Quotient ra and Quotient rb.

Русский

Эквивалентность e: α ≃ β с eq, связывающим ra и rb, индуцирует эквивалентность между Quotient ra и Quotient rb.

LaTeX

$$$ \mathrm{Quotient}\ congr\ e\ eq : Quotient ra \simeq Quotient rb $$$

Lean4

/-- An equivalence `e : α ≃ β` generates an equivalence between quotient spaces,
if `ra a₁ a₂ ↔ rb (e a₁) (e a₂)`. -/
protected def congr {ra : Setoid α} {rb : Setoid β} (e : α ≃ β) (eq : ∀ a₁ a₂, ra a₁ a₂ ↔ rb (e a₁) (e a₂)) :
    Quotient ra ≃ Quotient rb :=
  Quot.congr e eq

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