eventually_nnnorm_sub_lt — Mathlib

English

In a normed additive group, for any x0 and ε > 0, eventually x near x0 satisfy ∥x - x0∥₊ < ε.

Русский

В нормированной группе для любого x0 и ε > 0 существует окрестность x0 такая, что близкие точки удовлетворяют ∥x - x0∥₊ < ε.

LaTeX

$$$\forall x_0\in E\,\forall \varepsilon>0\,\forall^{\infty} x\to x_0, \|x- x_0\|_{+} < \varepsilon$$$

Lean4

theorem eventually_nnnorm_sub_lt (x₀ : E) {ε : ℝ≥0} (ε_pos : 0 < ε) : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖₊ < ε :=
  (continuousAt_id.sub continuousAt_const).nnnorm (gt_mem_nhds <| by simpa)

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