English
Let E be a normed space with q a seminorm-family; if there exists a bound of the form (q i).comp f ≤ C · normSeminorm on E for all i, then f is continuous.
Русский
Пусть E — нормированное пространство, q — семейство семинорм; если существует ограничение (q_i)∘f ≤ C·norm для каждого i, то f непрерывно.
LaTeX
$$$cont_normedSpace_to_withSeminorms:\\; (F)\\Rightarrow (\\forall i, \\exists C: \\mathbb{R}_{\\ge 0}, (q_i) \\circ f ≤ C \\cdot \\|\\cdot\\|)$$$
Lean4
theorem continuous_from_bounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'} {_ : TopologicalSpace E}
(hp : WithSeminorms p) {_ : TopologicalSpace F} (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F)
(hf : Seminorm.IsBounded p q f) : Continuous f :=
by
have : IsTopologicalAddGroup E := hp.topologicalAddGroup
refine continuous_of_continuous_comp hq _ fun i => ?_
rcases hf i with ⟨s, C, hC⟩
rw [← Seminorm.finset_sup_smul] at hC
refine Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)
change Continuous (fun x ↦ Seminorm.coeFnAddMonoidHom _ _ (∑ i ∈ s, C • p i) x)
simp_rw [map_sum, Finset.sum_apply]
exact (continuous_finset_sum _ fun i _ ↦ (hp.continuous_seminorm i).const_smul (C : ℝ))
