English
If p is continuous at 0 with respect to the addition structure and the space is uniform, then p is uniformly continuous.
Русский
Если p непрерывна в нуле (относительно структуры сложения и униформности пространства), то p является равномерно непрерывной.
LaTeX
$$$ \\text{ContinuousAt}(p,0) \\Rightarrow \\text{UniformContinuous}(p). $$$
Lean4
protected theorem uniformContinuous_of_continuousAt_zero [UniformSpace E] [IsUniformAddGroup E] {p : Seminorm 𝕝 E}
(hp : ContinuousAt p 0) : UniformContinuous p :=
by
have hp : Filter.Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp
rw [UniformContinuous, uniformity_eq_comap_nhds_zero_swapped, Metric.uniformity_eq_comap_nhds_zero,
Filter.tendsto_comap_iff]
exact
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hp.comp Filter.tendsto_comap) (fun xy => dist_nonneg)
fun xy => p.norm_sub_map_le_sub _ _
