English
If a map φ: H → α → E induces a topology on H from UniformFun and each φ(u) has uniformly bounded range, then H carries a continuous scalar action with respect to 𝕜.
Русский
Если отображение φ задаёт т.д. топологию на H и образ каждого φ(u) ограничен на α равномерно, то H имеет непрерывное действие скаляра 𝕜.
LaTeX
$$$IsInducing (ofFun \\circ φ) \\\\Rightarrow \\\\forall u, IsVonNBounded 𝕜 (Range(φ u)) \\\\Rightarrow 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.
For convenience, we don't literally ask for `H : Submodule (α →ᵤ[𝔖] E)`. Instead, we prove the
result for any vector space `H` equipped with a linear inducing to `α →ᵤ[𝔖] E`, which is often
easier to use. We also state the `Submodule` version as
`UniformOnFun.continuousSMul_submodule_of_image_bounded`. -/
theorem continuousSMul_induced_of_image_bounded (φ : hom) (hφ : IsInducing (ofFun 𝔖 ∘ φ))
(h : ∀ u : H, ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 ((φ u : α → E) '' s)) : ContinuousSMul 𝕜 H :=
by
obtain rfl := hφ.eq_induced; clear hφ
simp only [induced_iInf, UniformOnFun.topologicalSpace_eq, induced_compose]
refine continuousSMul_iInf fun s ↦ continuousSMul_iInf fun hs ↦ ?_
letI : TopologicalSpace H := .induced (UniformFun.ofFun ∘ s.restrict ∘ φ) (UniformFun.topologicalSpace s E)
set φ' : H →ₗ[𝕜] (s → E) :=
{ toFun := s.restrict ∘ φ, map_smul' := fun c x ↦ by exact congr_arg s.restrict (map_smul φ c x),
map_add' := fun x y ↦ by exact congr_arg s.restrict (map_add φ x y) }
refine UniformFun.continuousSMul_induced_of_range_bounded 𝕜 s E H φ' ⟨rfl⟩ fun u ↦ ?_
simpa only [Set.image_eq_range] using h u s hs
