homCongr_symm — Mathlib

English

The inverse of a homCongr is given by taking inverses of the constituting isomorphisms.

Русский

Обратный элемент к homCongr получается взятием обратных к составным изоморфизмам.

LaTeX

$$$ (\\alpha.homCongr \\beta)^{-1} = \\alpha^{-1}.homCongr \\beta^{-1} $$$

Lean4

@[simp]
theorem homCongr_symm {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂) : (α.homCongr β).symm = α.symm.homCongr β.symm :=
  rfl

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