English
The symm map evaluation at base point matches composing with e2.symmL and the inner map L composed with e1.continuousLinearMapAt.
Русский
Оценка симм отображения в базовой точке совпадает с композицией с e2.symmL и отображением L, композиция с e1.continuousLinearMapAt.
LaTeX
$$$ (continuousLinearMap σ e_1 e_2).symm_apply = (e_2.symmL 𝕜_2) \\circ (L \\circ (e_1.continuousLinearMapAt 𝕜_1)) $$$
Lean4
/-- Given trivializations `e₁`, `e₂` in the atlas for vector bundles `E₁`, `E₂` over a base `B`,
the induced trivialization for the continuous `σ`-semilinear maps from `E₁` to `E₂`,
whose base set is `e₁.baseSet ∩ e₂.baseSet`. -/
def continuousLinearMap : Trivialization (F₁ →SL[σ] F₂) (π (F₁ →SL[σ] F₂)(fun x ↦ E₁ x →SL[σ] E₂ x)) :=
VectorPrebundle.trivializationOfMemPretrivializationAtlas _ ⟨e₁, e₂, he₁, he₂, rfl⟩
