English
The topology induced by a seminorm-family p is the infimum of the topologies induced by each p_i; i.e., the space is exactly the infimum of the topologies coming from the seminorms p_i.
Русский
Топология, заданная семинормами p, равна наименьшей верхнепорядковой инфинумной топологии, порождаемой каждым p_i.
LaTeX
$$$WithSeminorms\\ p \\iff t = \\bigwedge_i (p_i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace$$$
Lean4
/-- The topology induced by a family of seminorms is exactly the infimum of the ones induced by
each seminorm individually. We express this as a characterization of `WithSeminorms p`. -/
theorem withSeminorms_iff_topologicalSpace_eq_iInf [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι) :
WithSeminorms p ↔ t = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace :=
by
rw [p.withSeminorms_iff_nhds_eq_iInf,
IsTopologicalAddGroup.ext_iff inferInstance (topologicalAddGroup_iInf fun i => inferInstance), nhds_iInf]
congrm _ = ⨅ i, ?_
exact @comap_norm_nhds_zero _ (p i).toSeminormedAddGroup
