topologicalSpaceTotalSpace — Mathlib

English

The total space topology on the bundle of continuous σ-linear maps is that of the associated vector prebundle, i.e. given by totalSpaceTopology.

Русский

Топология полного пространства для расслоения непрерывных σ‑линейных отображений задаётся через totalSpaceTopology связанного векторного предрасслоения.

LaTeX

$$$ \\text{topologicalSpaceTotalSpace } = \\text{vectorPrebundle}.totalSpaceTopology$$$

Lean4

/-- Topology on the total space of the continuous `σ`-semilinear maps between two "normable" vector
bundles over the same base. -/
instance topologicalSpaceTotalSpace : TopologicalSpace (TotalSpace (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x)) :=
  (Bundle.ContinuousLinearMap.vectorPrebundle σ F₁ E₁ F₂ E₂).totalSpaceTopology

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