continuous_of_continuousAt_zero — Mathlib

English

Under uniform structures, a continuousAt-zero implies uniform continuity for p.

Русский

При условии униформной структуры непрерывность в нуле имплицирует униформную непрерывность для p.

LaTeX

$$$ \\text{ContinuousAt}(p,0) \\Rightarrow \\text{UniformContinuous}(p). $$$

Lean4

protected theorem continuous_of_continuousAt_zero [TopologicalSpace E] [IsTopologicalAddGroup E] {p : Seminorm 𝕝 E}
    (hp : ContinuousAt p 0) : Continuous p :=
  by
  letI := IsTopologicalAddGroup.toUniformSpace E
  haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  exact (Seminorm.uniformContinuous_of_continuousAt_zero hp).continuous

Похожие утверждения