English
If for every i the seminorm family p_i has the withSeminorms property, then the sigma construction over i of (p_i).comp (LinearMap.proj i) yields a seminorm family with withSeminorms on the product space.
Русский
Если для каждого i семейство p_i имеет свойство withSeminorms, то сигма-конструкция над i от (p_i).comp (LinearMap.proj i) образует семейство семинорм на произведении, обладающее withSeminorms.
LaTeX
$$$ withSeminorms_iInf (\\ λ i, WithSeminorms (p i)) \\Rightarrow WithSeminorms (SeminormFamily.sigma (fun i => (p i).comp (LinearMap.proj i))) $$$
Lean4
theorem withSeminorms_pi {κ : ι → Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
[∀ i, TopologicalSpace (E i)] {p : (i : ι) → SeminormFamily 𝕜 (E i) (κ i)} (hp : ∀ i, WithSeminorms (p i)) :
WithSeminorms (SeminormFamily.sigma (fun i ↦ (p i).comp (LinearMap.proj i))) :=
withSeminorms_iInf fun i ↦ (LinearMap.proj i).withSeminorms_induced (hp i)
