continuousLinearMap_apply — Mathlib

English

The inverse of the continuousLinearMap preorder trivialization at a base point b acts by composing with the coordinatewise inverse maps on the two fibers.

Русский

Обратное отображение претривиализации действует через композицию с обратными координатными отображениями на двух волокнах над b.

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_apply (p : TotalSpace (F₁ →SL[σ] F₂) fun x ↦ E₁ x →SL[σ] E₂ x) :
    (continuousLinearMap σ e₁ e₂) p = ⟨p.1, .comp (e₂.continuousLinearMapAt 𝕜₂ p.1) (p.2.comp (e₁.symmL 𝕜₁ p.1))⟩ :=
  rfl

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