English
If a seminorm family p has a basis of neighborhoods given by a basis of the zero neighborhood, then WithSeminorms p holds.
Русский
Если у семейства семинорм p есть база окрестностей нуля, заданная базисом нулевой окрестности, то WithSeminorms p выполняется.
LaTeX
$$$WithSeminorms\\ p$ \n (basis condition) $$
Lean4
/-- The uniform structure 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_uniformSpace_eq_iInf [u : UniformSpace E] [IsUniformAddGroup E] (p : SeminormFamily 𝕜 E ι) :
WithSeminorms p ↔ u = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace :=
by
rw [p.withSeminorms_iff_nhds_eq_iInf,
IsUniformAddGroup.ext_iff inferInstance (isUniformAddGroup_iInf fun i => inferInstance),
UniformSpace.toTopologicalSpace_iInf, nhds_iInf]
congrm _ = ⨅ i, ?_
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup
