arrowCongr_trans — Mathlib

English

Applying the arrowCongr to a linear map f and vector x yields e_2 (f (e_1^{-1} x)).

Русский

Применение стрелочного конгрунта к линейному отображению и вектору даёт e_2 (f (e_1^{-1} x)).

LaTeX

$$$arrowCongr e_1 e_2 f x = e_2 (f (e_1^{-1} x))$$$

Lean4

theorem arrowCongr_trans (e₁ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₁' : M₁' ≃ₛₗ[σ₁'₂'] M₂') (e₂ : M₂ ≃ₛₗ[σ₂₃] M₃)
    (e₂' : M₂' ≃ₛₗ[σ₂'₃'] M₃') :
    ((arrowCongr e₁ e₁').trans (arrowCongr e₂ e₂' : (M₂ →ₛₗ[σ₂₂'] M₂') ≃ₛₗ[σ₂'₃'] _)) =
      arrowCongr (e₁.trans e₂) (e₁'.trans e₂') :=
  rfl

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