English
Let H be a submodule of α →ᵤ[𝔖] E, and suppose every image of a set S ∈ 𝔖 under any u ∈ H is bounded. Then H, with the induced UniformOnFun topology from α →ᵤ[𝔖] E, becomes a topological vector space over 𝕜.
Русский
Пусть H — подмодуль α →ᵤ[𝔖] E, и пусть образ каждого S ∈ 𝔖 под любым u ∈ H ограничен. Тогда H с индуцированной топологией UniformOnFun становится топологическим векторным пространством над 𝕜.
LaTeX
$$$H \\text{ Submodule},\\forall u \\in H,\\forall S\\in 𝔖, Bornology.IsVonNBounded 𝕜 (u'' S) \\\\Rightarrow \\\\text{ContinuousSMul 𝕜 } H$$$
Lean4
/-- Let `E` be a TVS, `𝔖 : Set (Set α)` and `H` a submodule of `α →ᵤ[𝔖] E`. If the image of any
`S ∈ 𝔖` by any `u ∈ H` is bounded (in the sense of `Bornology.IsVonNBounded`), then `H`,
equipped with the topology of `𝔖`-convergence, is a TVS.
If you have a hard time using this lemma, try the one above instead. -/
theorem continuousSMul_submodule_of_image_bounded (H : Submodule 𝕜 (α →ᵤ[𝔖] E))
(h : ∀ u ∈ H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (u '' s)) :
@ContinuousSMul 𝕜 H _ _ ((UniformOnFun.topologicalSpace α E 𝔖).induced ((↑) : H → α →ᵤ[𝔖] E)) :=
UniformOnFun.continuousSMul_induced_of_image_bounded 𝕜 α E H (LinearMap.id.domRestrict H : H →ₗ[𝕜] α → E)
IsInducing.subtypeVal fun ⟨u, hu⟩ => h u hu
