self_comp_symm

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.self_comp_symm

English

If e1: M1 ≃SL[σ₁₂] M2 and e2: M2 ≃SL[σ₂₃] M3, then (e1.trans e2) applied to c equals e2 applied to e1 applied to c.

Русский

Если e1: M1 ≃SL[σ₁₂] M2 и e2: M2 ≃SL[σ₂₃] M3, то (e1.trans e2)(c) = e2(e1(c)).

LaTeX

$$$ (e_1 \\trans e_2)(c) = e_2(e_1(c)) $$$

Lean4

@[simp]
theorem self_comp_symm (e : M₁ ≃SL[σ₁₂] M₂) : (e : M₁ → M₂) ∘ (e.symm : M₂ → M₁) = id :=
  by
  ext x
  exact apply_symm_apply e x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru