coe_comp_coe_symm — Mathlib

English

The coherent composition of two coerced linear maps matches the composition of the corresponding continuous linear equivalences.

Русский

Согласованная композиция приведённых линейных отображений совпадает с композицией соответствующих непрерывных линейных эквивалентов.

LaTeX

$$$ (f' : M_2 \\toSL[\\sigma_{23}] M_3).comp (f : M_1 \\toSL[\\sigma_{12}] M_2) = (f.trans f') $$$

Lean4

@[simp high]
theorem coe_comp_coe_symm (e : M₁ ≃SL[σ₁₂] M₂) :
    (e : M₁ →SL[σ₁₂] M₂).comp (e.symm : M₂ →SL[σ₂₁] M₁) = ContinuousLinearMap.id R₂ M₂ :=
  ContinuousLinearMap.ext e.apply_symm_apply

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