English
The uniform structure induced by p is the infimum of the ones given by each p_i; i.e., WithSeminorms p iff the uniform space equals iInf of the p_i-induced uniform spaces.
Русский
Унитарная структура, индуцированная p, равна инф-минивому пространству структур, индуцированных каждым p_i.
LaTeX
$$$WithSeminorms\\ p \\iff u = \\bigwedge_i (p_i).toSeminormedAddCommGroup.toUniformSpace$$$
Lean4
/-- The topology of a `NormedSpace 𝕜 E` is induced by the seminorm `normSeminorm 𝕜 E`. -/
theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
WithSeminorms fun _ : Fin 1 => normSeminorm 𝕜 E := by
rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm, comap_norm_nhds_zero]
