equivCongr_trans — Mathlib

English

The equivCongr construction is functorial in both arguments with respect to composition and symmetry: (equivCongr e1 e1').trans (equivCongr e2 e2') = equivCongr (e1.trans e2) (e1'.trans e2').

Русский

Конструкция equivCongr связана по композиции и симметрии между двумя парами изоморфизмов.

LaTeX

$$$\\text{equivCongr }(e_1,e_1')\\trans (equivCongr e_2,e_2') = equivCongr (e_1\\trans e_2) (e_1'\\trans e_2').$$$

Lean4

@[simp]
theorem equivCongr_trans (e₁₂ : A₁ ≃ₐ[R] A₂) (e₁₂' : A₁' ≃ₐ[R] A₂') (e₂₃ : A₂ ≃ₐ[R] A₃) (e₂₃' : A₂' ≃ₐ[R] A₃') :
    (equivCongr e₁₂ e₁₂').trans (equivCongr e₂₃ e₂₃') = equivCongr (e₁₂.trans e₂₃) (e₁₂'.trans e₂₃') :=
  rfl

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