Mathlib.Analysis.Normed.Group.Lemmas

Module docstring

{"# Further lemmas about normed groups

This file contains further lemmas about normed groups, requiring heavier imports than Mathlib/Analysis/Normed/Group/Basic.lean.

TODO

Move lemmas from Basic to other places, including this file.

eventually_nnnorm_sub_lt theorem

(x₀ : E) {ε : ℝ≥0} (ε_pos : 0 < ε) : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖₊ < ε

Full source

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)

Neighborhood Points Have Seminorm Difference Less Than Epsilon

Informal description

For any point $x₀$ in a seminormed additive commutative group $E$ and any positive real number $\varepsilon > 0$, the set of all points $x$ in a neighborhood of $x₀$ such that the seminorm $\|x - x₀\|₊$ is less than $\varepsilon$ is eventually true.

eventually_norm_sub_lt theorem

(x₀ : E) {ε : ℝ} (ε_pos : 0 < ε) : ∀ᶠ x in 𝓝 x₀, ‖x - x₀‖ < ε

Full source

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)

Neighborhood Points Have Norm Difference Less Than Epsilon

Informal description

For any point $x_0$ in a seminormed additive commutative group $E$ and any positive real number $\varepsilon > 0$, the set of all points $x$ in a neighborhood of $x_0$ such that the norm $\|x - x_0\|$ is less than $\varepsilon$ is eventually true.