continuousAt_zero — Mathlib

English

If p.ball 0 r ∈ 𝓝 0 for some r>0, then p is continuous at 0.

Русский

Если существует r>0 такое, что p.ball 0 r ∈ 𝓝 0, то p непрерывна в 0.

LaTeX

$$$ \\exists r>0:\\; p.\\mathrm{ball}(0,r) \\in \\mathcal{N}_0 \\Rightarrow \\text{ContinuousAt}(p,0). $$$

Lean4

theorem continuousAt_zero [TopologicalSpace E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E} {r : ℝ}
    (hp : p.ball 0 r ∈ (𝓝 0 : Filter E)) : ContinuousAt p 0 :=
  continuousAt_zero' (Filter.mem_of_superset hp <| p.ball_subset_closedBall _ _)

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