continuousLinearMap_symm_apply' — Mathlib

English

For base point b in e1.baseSet and e2.baseSet, the symm application at b to L is given by the composition with e2.symmL and L composed with e1.continuousLinearMapAt.

Русский

Для основания b из e1.baseSet и e2.baseSet, симм приложение в b к L задаётся композицией с e2.symmL и L, композиция с e1.continuousLinearMapAt.

LaTeX

$$$ (continuousLinearMap σ e_1 e_2).symm b L = (e_2.symmL 𝕜_2 b) \\circ (L \\circ (e_1.continuousLinearMapAt 𝕜_1 b)) $$$

Lean4

theorem continuousLinearMap_symm_apply' {b : B} (hb : b ∈ e₁.baseSet ∩ e₂.baseSet) (L : F₁ →SL[σ] F₂) :
    (continuousLinearMap σ e₁ e₂).symm b L = (e₂.symmL 𝕜₂ b).comp (L.comp <| e₁.continuousLinearMapAt 𝕜₁ b) :=
  by
  rw [symm_apply]
  · rfl
  · exact hb

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