English
The fiberwise space of continuous σ-semilinear maps between two vector bundles forms a fiber bundle over the base with fiber being the space of maps E1(b) →SL[σ] E2(b).
Русский
Фибровое пространство непрерывных σ‑полу-линейных отображений между двумя векторными расслоениями образует расслоение над базой, где волокно равно множеству отображений E1(b) →SL[σ] E2(b).
LaTeX
$$$\\text{FiberBundle } (F_1 \\toSL[σ] F_2)\\; (\\,b \\mapsto E_1(b) \\toSL[σ] E_2(b)\\,)$$$
Lean4
/-- A reducible type synonym for the bundle of continuous (semi)linear maps. -/
@[deprecated "Use the plain bundle syntax `fun (b : B) ↦ E₁ b →SL[σ] E₂ b` or
`fun (b : B) ↦ E₁ b →L[𝕜] E₂ b` instead" (since := "2025-06-12")]
protected abbrev ContinuousLinearMap [∀ x, TopologicalSpace (E₁ x)] [∀ x, TopologicalSpace (E₂ x)] : B → Type _ :=
fun x ↦ E₁ x →SL[σ] E₂ x
