English
Let X be a topological space and let g: X → L(F,G) be a continuous family of continuous linear maps, while f: E → L(F,G) is fixed. Then x ↦ (g(x)) ∘ f is a continuous map from X into L(E,G).
Русский
Пусть X — топологическое пространство, g: X → L(F,G) — непрерывная семейство линейных отображений, а f: E → L(F,G) фиксировано. Тогда отображение x ↦ g(x) ∘ f непрерывно как отображение X → L(E,G).
LaTeX
$$$X\text{ топологическое пространство},\ g: X \to L(F,G),\ f: E \to L(F,G)\text{ фиксировано}.\ If\ g\text{ непрерывно на }X,\ then\ x \mapsto g(x) \circ f\;\text{ является непрерывным отображением }X\text{ в }L(E,G).$$$
Lean4
theorem _root_.Continuous.clm_comp_const {X} [TopologicalSpace X] {g : X → F →SL[σ₂₃] G} (hg : Continuous g)
(f : E →SL[σ₁₂] F) : Continuous (fun x => (g x).comp f : X → E →SL[σ₁₃] G) :=
(@ContinuousLinearMap.flip _ _ _ _ _ (E →SL[σ₁₃] G) _ _ _ _ _ _ _ _ _ _ _ _ _ (compSL E F G σ₁₂ σ₂₃)
f).continuous.comp
hg
