English
A linear map is continuous if and only if all its seminorm compositions with the seminorm family are continuous.
Русский
Линейное отображение непрерывно тогда и только тогда, когда все его композиции с семинормами непрерывны.
LaTeX
$$$WithSeminorms\\ q \\Rightarrow (Continuous f \\iff ∀ i, Continuous ((q_i)\\circ f))$$$
Lean4
theorem continuous_of_continuous_comp {q : SeminormFamily 𝕝₂ F ι'} [TopologicalSpace E] [IsTopologicalAddGroup E]
[TopologicalSpace F] (hq : WithSeminorms q) (f : E →ₛₗ[τ₁₂] F) (hf : ∀ i, Continuous ((q i).comp f)) :
Continuous f := by
have : IsTopologicalAddGroup F := hq.topologicalAddGroup
refine continuous_of_continuousAt_zero f ?_
simp_rw [ContinuousAt, f.map_zero, q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.tendsto_iInf,
Filter.tendsto_comap_iff]
intro i
convert (hf i).continuousAt.tendsto
exact (map_zero _).symm
