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₀‖₊ < ε

@[deprecated eventually_nnNorm_sub_lt (since := "2026-10-31")]

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

Alias of eventually_nnNorm_sub_lt.

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

theorem Subgroup.dense_of_infDist_le {G : Type u_2} [SeminormedGroup G] (H : Subgroup G) (ε : ℝ) (h1 : 0 < ε) (h2 : ε < 1) (h : ∀ (g : G), Metric.infDist g ↑H ≤ ε * ‖g‖) : Dense ↑H

Let G be a seminormed group. If a subgroup H is ε-dense for some ε < 1, that is infDist g H ≤ ε * ‖g‖ for every g : G, then H is dense. This is [BGR, Prop 1.1.4./2][bosch-guntzer-remmert].

theorem AddSubgroup.dense_of_infDist_le {G : Type u_2} [SeminormedAddGroup G] (H : AddSubgroup G) (ε : ℝ) (h1 : 0 < ε) (h2 : ε < 1) (h : ∀ (g : G), Metric.infDist g ↑H ≤ ε * ‖g‖) : Dense ↑H