English
Given a family of topologies t_i on E, the iInf (infimum over i) of these topologies can be represented via a sigma-type of the corresponding seminorm families, yielding a combined topology.
Русский
При задании топологий t_i на E инфимум по i можно представить через сигма-тип соответствующих семинарорм, образуя объединённую топологию.
LaTeX
$$$ withSeminorms_iInf \\ (p) : WithSeminorms (SeminormFamily.sigma p) $$$
Lean4
theorem withSeminorms_iInf {κ : ι → Type*} {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E}
(hp : ∀ i, WithSeminorms (topology := t i) (p i)) : WithSeminorms (topology := ⨅ i, t i) (SeminormFamily.sigma p) :=
by
have : ∀ i, @IsTopologicalAddGroup E (t i) _ := fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ (t i) _ (hp i)
have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance
simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢
rw [iInf_sigma]
exact iInf_congr hp
