English
Locally around any basepoint x, the operator norm of the composed trivialization maps is bounded by a universal bound approaching 1 from above.
Русский
В окрестности любой точки базаx нормa композиции тривиализации ограничена верхней границей, стремящейся к 1.
LaTeX
$$$\\forall x, \\exists C>0, \\forall y\\to x: \\|((trivializationAt F E x).symmL \\mathbb{R} x) \\circL ((trivializationAt F E x).continuousLinearMapAt \\mathbb{R} y)\\| < C$$$
Lean4
/-- Rewrite `ContinuousLinearMap.inCoordinates` using continuous linear equivalences, in the
bundle of bilinear maps. -/
theorem inCoordinates_apply_eq₂ {x₀ x : B} {ϕ : E₁ x →L[𝕜] E₂ x →L[𝕜] E₃ x} {v : F₁} {w : F₂}
(h₁x : x ∈ (trivializationAt F₁ E₁ x₀).baseSet) (h₂x : x ∈ (trivializationAt F₂ E₂ x₀).baseSet)
(h₃x : x ∈ (trivializationAt F₃ E₃ x₀).baseSet) :
inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃) (fun x ↦ E₂ x →L[𝕜] E₃ x) x₀ x x₀ x ϕ v w =
(trivializationAt F₃ E₃ x₀).linearMapAt 𝕜 x
(ϕ ((trivializationAt F₁ E₁ x₀).symm x v) ((trivializationAt F₂ E₂ x₀).symm x w)) :=
by
rw [inCoordinates_eq h₁x (by simp [h₂x, h₃x])]
simp [hom_trivializationAt, Trivialization.continuousLinearMap_apply]
