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.

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

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