# 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.

source
theorem eventually_nnnorm_sub_lt {E : Type u_1} [SeminormedAddCommGroup E] (x₀ : E) {ε : NNReal} (ε_pos : 0 < ε) :
∀ᶠ (x : E) in nhds x₀, ‖x - x₀‖₊ < ε
source
theorem eventually_norm_sub_lt {E : Type u_1} [SeminormedAddCommGroup E] (x₀ : E) {ε : ℝ} (ε_pos : 0 < ε) :
∀ᶠ (x : E) in nhds x₀, ‖x - x₀‖ < ε