eventually_norm_sub_lt — Mathlib

English

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

Русский

В нормированной группе существует окрестность 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_norm_sub_lt (x₀ : E) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖ < ε :=
  (continuousAt_id.sub continuousAt_const).norm (gt_mem_nhds <| by simpa)

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