English
From a countable family of seminorms p_i on the components E_i, the combined family sigma of (p_i).comp (proj i) again yields a withSeminorms topology on the product space, preserving local convexity and the induced topology when forming the sigma construction.
Русский
Из счетного набора семинорм p_i на компонентах E_i совокупность sigma от (p_i).comp (proj i) снова порождает топологию с withSeminorms на произведении, сохраняя локальную выпуклость и индуцированную топологию при сигма-конструкции.
LaTeX
$$$ withSeminorms (p i).comp (LinearMap.proj i) \\Rightarrow withSeminorms (SeminormFamily.sigma (fun i => (p i).comp (LinearMap.proj i))) $$$
Lean4
theorem withSeminorms_induced {q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) (f : E →ₛₗ[σ₁₂] F) :
WithSeminorms (topology := induced f inferInstance) (q.comp f) :=
by
have := hq.topologicalAddGroup
let _ : TopologicalSpace E := induced f inferInstance
have : IsTopologicalAddGroup E := topologicalAddGroup_induced f
rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero, q.withSeminorms_iff_nhds_eq_iInf.mp hq,
Filter.comap_iInf]
refine iInf_congr fun i => ?_
exact Filter.comap_comap
