# Continuity of the norm on (semi)groups #

## Tags #

normed group

source
theorem tendsto_iff_norm_div_tendsto_zero {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {a : Filter α} {b : E} :
Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e / b‖) a (nhds 0)
source
theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E} :
Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e - b‖) a (nhds 0)
source
theorem tendsto_one_iff_norm_tendsto_zero {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {a : Filter α} :
Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)
source
theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {a : Filter α} :
Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)
source
@[simp]
theorem comap_norm_nhds_one {E : Type u_5} [SeminormedGroup E] :
Filter.comap norm (nhds 0) = nhds 1
source
@[simp]
theorem comap_norm_nhds_zero {E : Type u_5} [SeminormedAddGroup E] :
Filter.comap norm (nhds 0) = nhds 0
source
theorem squeeze_one_norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : Filter.Tendsto a t₀ (nhds 0)) :
Filter.Tendsto f t₀ (nhds 1)

Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real function `a` which tends to `0`, then `f` tends to `1` (neutral element of `SeminormedGroup`). In this pair of lemmas (`squeeze_one_norm'` and `squeeze_one_norm`), following a convention of similar lemmas in `Topology.MetricSpace.Basic` and `Topology.Algebra.Order`, the `'` version is phrased using "eventually" and the non-`'` version is phrased absolutely.

source
theorem squeeze_zero_norm' {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) (h' : Filter.Tendsto a t₀ (nhds 0)) :
Filter.Tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real function `a` which tends to `0`, then `f` tends to `0`. In this pair of lemmas (`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of similar lemmas in `Topology.MetricSpace.Pseudo.Defs` and `Topology.Algebra.Order`, the `'` version is phrased using "eventually" and the non-`'` version is phrased absolutely.

source
theorem squeeze_one_norm {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ (n : α), ‖f n‖ ≤ a n) :
Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)

Special case of the sandwich theorem: if the norm of `f` is bounded by a real function `a` which tends to `0`, then `f` tends to `1`.

source
theorem squeeze_zero_norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α} (h : ∀ (n : α), ‖f n‖ ≤ a n) :
Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)

Special case of the sandwich theorem: if the norm of `f` is bounded by a real function `a` which tends to `0`, then `f` tends to `0`.

source
theorem tendsto_norm_div_self {E : Type u_5} [SeminormedGroup E] (x : E) :
Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhds 0)
source
theorem tendsto_norm_sub_self {E : Type u_5} [SeminormedAddGroup E] (x : E) :
Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhds 0)
source
theorem tendsto_norm_div_self_nhdsGE {E : Type u_5} [SeminormedGroup E] (x : E) :
Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
source
theorem tendsto_norm_sub_self_nhdsGE {E : Type u_5} [SeminormedAddGroup E] (x : E) :
Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))
source
theorem tendsto_norm' {E : Type u_5} [SeminormedGroup E] {x : E} :
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)
source
theorem tendsto_norm {E : Type u_5} [SeminormedAddGroup E] {x : E} :
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)
source
theorem tendsto_norm_one {E : Type u_5} [SeminormedGroup E] :
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 1) (nhds 0)

See `tendsto_norm_one` for a version with pointed neighborhoods.

source
theorem tendsto_norm_zero {E : Type u_5} [SeminormedAddGroup E] :
Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 0) (nhds 0)

See `tendsto_norm_zero` for a version with pointed neighborhoods.

source
theorem continuous_norm' {E : Type u_5} [SeminormedGroup E] :
Continuous fun (a : E) => ‖a‖
source
theorem continuous_norm {E : Type u_5} [SeminormedAddGroup E] :
Continuous fun (a : E) => ‖a‖
source
theorem continuous_nnnorm' {E : Type u_5} [SeminormedGroup E] :
Continuous fun (a : E) => ‖a‖₊
source
theorem continuous_nnnorm {E : Type u_5} [SeminormedAddGroup E] :
Continuous fun (a : E) => ‖a‖₊
source
instance SeminormedGroup.toContinuousENorm {E : Type u_5} [SeminormedGroup E] :
ContinuousENorm E
Equations

- SeminormedGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }

source
instance SeminormedAddGroup.toContinuousENorm {E : Type u_5} [SeminormedAddGroup E] :
ContinuousENorm E
Equations

- SeminormedAddGroup.toContinuousENorm = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯ }

source
instance NormedGroup.toENormedMonoid {F : Type u_8} [NormedGroup F] :
ENormedMonoid F
Equations

- NormedGroup.toENormedMonoid = { toContinuousENorm := SeminormedGroup.toContinuousENorm, toMonoid := inst✝.toMonoid, enorm_zero := ⋯, enorm_mul_le := ⋯, enorm_eq_zero := ⋯ }

source
instance NormedAddGroup.toENormedAddMonoid {F : Type u_8} [NormedAddGroup F] :
ENormedAddMonoid F
Equations

- NormedAddGroup.toENormedAddMonoid = { toContinuousENorm := SeminormedAddGroup.toContinuousENorm, toAddMonoid := inst✝.toAddMonoid, enorm_zero := ⋯, enorm_add_le := ⋯, enorm_eq_zero := ⋯ }

source
instance NormedCommGroup.toENormedCommMonoid {E : Type u_5} [NormedCommGroup E] :
ENormedCommMonoid E
Equations

- NormedCommGroup.toENormedCommMonoid = { toESeminormedMonoid := NormedGroup.toENormedMonoid.toESeminormedMonoid, mul_comm := ⋯, enorm_eq_zero := ⋯ }

source
instance NormedAddCommGroup.toENormedAddCommMonoid {E : Type u_5} [NormedAddCommGroup E] :
ENormedAddCommMonoid E
Equations

- NormedAddCommGroup.toENormedAddCommMonoid = { toESeminormedAddMonoid := NormedAddGroup.toENormedAddMonoid.toESeminormedAddMonoid, add_comm := ⋯, enorm_eq_zero := ⋯ }

source
theorem Inseparable.norm_eq_norm' {E : Type u_5} [SeminormedGroup E] {u v : E} (h : Inseparable u v) :
‖u‖ = ‖v‖
source
theorem Inseparable.norm_eq_norm {E : Type u_5} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) :
‖u‖ = ‖v‖
source
theorem Inseparable.nnnorm_eq_nnnorm' {E : Type u_5} [SeminormedGroup E] {u v : E} (h : Inseparable u v) :
‖u‖₊ = ‖v‖₊
source
theorem Inseparable.nnnorm_eq_nnnorm {E : Type u_5} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) :
‖u‖₊ = ‖v‖₊
source
theorem Inseparable.enorm_eq_enorm' {E : Type u_8} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) :
‖u‖ₑ = ‖v‖ₑ
source
theorem Inseparable.enorm_eq_enorm {E : Type u_8} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) :
‖u‖ₑ = ‖v‖ₑ
source
theorem mem_closure_one_iff_norm {E : Type u_5} [SeminormedGroup E] {x : E} :
x ∈ closure {1} ↔ ‖x‖ = 0
source
theorem mem_closure_zero_iff_norm {E : Type u_5} [SeminormedAddGroup E] {x : E} :
x ∈ closure {0} ↔ ‖x‖ = 0
source
theorem closure_one_eq {E : Type u_5} [SeminormedGroup E] :
closure {1} = {x : E | ‖x‖ = 0}
source
theorem closure_zero_eq {E : Type u_5} [SeminormedAddGroup E] :
closure {0} = {x : E | ‖x‖ = 0}
source
theorem Filter.Tendsto.norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)
source
theorem Filter.Tendsto.norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)
source
theorem Filter.Tendsto.nnnorm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)
source
theorem Filter.Tendsto.nnnorm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)
source
theorem Continuous.norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} :
Continuous f → Continuous fun (x : α) => ‖f x‖
source
theorem Continuous.norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} :
Continuous f → Continuous fun (x : α) => ‖f x‖
source
theorem Continuous.nnnorm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} :
Continuous f → Continuous fun (x : α) => ‖f x‖₊
source
theorem Continuous.nnnorm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} :
Continuous f → Continuous fun (x : α) => ‖f x‖₊
source
theorem Filter.Tendsto.enorm' {α : Type u_2} {E : Type u_5} [TopologicalSpace E] [ContinuousENorm E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖ₑ) l (nhds ‖a‖ₑ)
source
theorem Filter.Tendsto.enorm {α : Type u_2} {E : Type u_5} [TopologicalSpace E] [ContinuousENorm E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) :
Tendsto (fun (x : α) => ‖f x‖ₑ) l (nhds ‖a‖ₑ)
source
theorem ContinuousAt.norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :
ContinuousAt (fun (x : α) => ‖f x‖) a
source
theorem ContinuousAt.norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :
ContinuousAt (fun (x : α) => ‖f x‖) a
source
theorem ContinuousAt.nnnorm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :
ContinuousAt (fun (x : α) => ‖f x‖₊) a
source
theorem ContinuousAt.nnnorm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) :
ContinuousAt (fun (x : α) => ‖f x‖₊) a
source
theorem ContinuousWithinAt.norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => ‖f x‖) s a
source
theorem ContinuousWithinAt.norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => ‖f x‖) s a
source
theorem ContinuousWithinAt.nnnorm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a
source
theorem ContinuousWithinAt.nnnorm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) :
ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a
source
theorem ContinuousOn.norm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :
ContinuousOn (fun (x : α) => ‖f x‖) s
source
theorem ContinuousOn.norm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :
ContinuousOn (fun (x : α) => ‖f x‖) s
source
theorem ContinuousOn.nnnorm' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :
ContinuousOn (fun (x : α) => ‖f x‖₊) s
source
theorem ContinuousOn.nnnorm {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) :
ContinuousOn (fun (x : α) => ‖f x‖₊) s
source
theorem eventually_ne_of_tendsto_norm_atTop' {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {l : Filter α} {f : α → E} (h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop) (x : E) :
∀ᶠ (y : α) in l, f y ≠ x

If `‖y‖ → ∞`, then we can assume `y ≠ x` for any fixed `x`.

source
theorem eventually_ne_of_tendsto_norm_atTop {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {l : Filter α} {f : α → E} (h : Filter.Tendsto (fun (y : α) => ‖f y‖) l Filter.atTop) (x : E) :
∀ᶠ (y : α) in l, f y ≠ x

If `‖y‖→∞`, then we can assume `y≠x` for any fixed `x`

source
theorem SeminormedCommGroup.mem_closure_iff {E : Type u_5} [SeminormedGroup E] {s : Set E} {a : E} :
a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε
source
theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_5} [SeminormedAddGroup E] {s : Set E} {a : E} :
a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε
source
theorem SeminormedGroup.tendstoUniformlyOn_one {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
source
theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
TendstoUniformlyOn f 0 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε
source
theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedGroup G] {f : ι → κ → G} {l : Filter ι} {l' : Filter κ} :
UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) l'
source
theorem SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedAddGroup G] {f : ι → κ → G} {l : Filter ι} {l' : Filter κ} :
UniformCauchySeqOnFilter f l l' ↔ TendstoUniformlyOnFilter (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) l'
source
theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z / f n.2 z) 1 (l ×ˢ l) s
source
theorem SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero {ι : Type u_3} {κ : Type u_4} {G : Type u_7} [SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} :
UniformCauchySeqOn f l s ↔ TendstoUniformlyOn (fun (n : ι × ι) (z : κ) => f n.1 z - f n.2 z) 0 (l ×ˢ l) s
source
theorem controlled_prod_of_mem_closure {E : Type u_5} [SeminormedCommGroup E] {a : E} {s : Subgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 / a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
source
theorem controlled_sum_of_mem_closure {E : Type u_5} [SeminormedAddCommGroup E] {a : E} {s : AddSubgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) :
∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧ (∀ (n : ℕ), v n ∈ s) ∧ ‖v 0 - a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
source
theorem controlled_prod_of_mem_closure_range {E : Type u_5} {F : Type u_6} [SeminormedCommGroup E] [SeminormedCommGroup F] {j : E →* F} {b : F} (hb : b ∈ closure ↑j.range) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :
∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∏ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
source
theorem controlled_sum_of_mem_closure_range {E : Type u_5} {F : Type u_6} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {j : E →+ F} {b : F} (hb : b ∈ closure ↑j.range) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) :
∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range (n + 1), j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) - b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n
source
theorem tendsto_norm_nhdsNE_one {E : Type u_5} [NormedGroup E] :
Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

See `tendsto_norm_one` for a version with full neighborhoods.

source
theorem tendsto_norm_nhdsNE_zero {E : Type u_5} [NormedAddGroup E] :
Filter.Tendsto norm (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

See `tendsto_norm_zero` for a version with full neighborhoods.

source
theorem tendsto_norm_div_self_nhdsNE {E : Type u_5} [NormedGroup E] (a : E) :
Filter.Tendsto (fun (x : E) => ‖x / a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
source
theorem tendsto_norm_sub_self_nhdsNE {E : Type u_5} [NormedAddGroup E] (a : E) :
Filter.Tendsto (fun (x : E) => ‖x - a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
source
theorem comap_norm_nhdsGT_zero' (E : Type u_5) [NormedGroup E] :
Filter.comap norm (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 1 {1}ᶜ

A version of `comap_norm_nhdsGT_zero` for a multiplicative normed group.

source
theorem comap_norm_nhdsGT_zero (E : Type u_5) [NormedAddGroup E] :
Filter.comap norm (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 0 {0}ᶜ