continuous_iff — Mathlib

English

If the closed balls around 0 lie inside neighborhoods of 0 for all radii, then p is continuous at 0.

Русский

Если все замкнутые шары вокруг 0 лежат в окрестностях 0, то p непрерывна в 0.

LaTeX

$$$ \\forall r>0:\\; p.\\overline{Ball}(0,r) \\in 𝓝 0 \\Rightarrow \\text{ContinuousAt}(p,0). $$$

Lean4

protected theorem continuous_iff [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
    {p : Seminorm 𝕜 E} {r : ℝ} (hr : 0 < r) : Continuous p ↔ p.ball 0 r ∈ 𝓝 0 :=
  ⟨fun H ↦ p.ball_zero_eq ▸ (H.tendsto' 0 0 (map_zero p)).eventually_lt_const hr, p.continuous⟩

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