continuousLinearMap — Mathlib

English

The space of continuous linear maps between fibers forms a ContMDiff vector bundle over the base manifold, rendering a compatible differential structure for fiberwise linear morphisms.

Русский

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

LaTeX

$$$\\text{ContMDiffVectorBundle.continuousLinearMap}$$$

Lean4

instance continuousLinearMap : ContMDiffVectorBundle n (F₁ →L[𝕜] F₂) ((fun (b : B) ↦ E₁ b →L[𝕜] E₂ b)) IB :=
  (Bundle.ContinuousLinearMap.vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).contMDiffVectorBundle IB

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