continuous — Mathlib

English

If for all r>0 the ball B(0,r) is in 𝓝 0, then p is continuous.

Русский

Если для всех r>0 шар B(0,r) лежит в 𝓝 0, то p непрерывна.

LaTeX

$$$ \\forall r>0:\\; p.ball(0,r) \\in 𝓝 0 \\Rightarrow \\text{Continuous}(p). $$$

Lean4

protected theorem continuous [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E}
    {r : ℝ} (hp : p.ball 0 r ∈ (𝓝 0 : Filter E)) : Continuous p :=
  Seminorm.continuous_of_continuousAt_zero (continuousAt_zero hp)

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