Continuity of the norm on (semi)normed groups

Tags

normed group

theorem continuous_enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] : Continuous fun (a : E) => ‖a‖ₑ

theorem Continuous.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} : Continuous f → Continuous fun (x : X) => ‖f x‖ₑ

theorem ContinuousAt.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {a : X} (h : ContinuousAt f a) : ContinuousAt (fun (x : X) => ‖f x‖ₑ) a

theorem ContinuousWithinAt.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {s : Set X} {a : X} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : X) => ‖f x‖ₑ) s a

theorem ContinuousOn.enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {X : Type u_8} [TopologicalSpace X] {f : X → E} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (fun (x : X) => ‖f x‖ₑ) s

theorem tendsto_iff_norm_inv_mul_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖(f e)⁻¹ * b‖) a (nhds 0)

theorem tendsto_iff_norm_neg_add_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖-f e + b‖) a (nhds 0)

theorem tendsto_one_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} : Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)

theorem tendsto_zero_iff_norm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} : Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)

theorem tendsto_iff_enorm_inv_mul_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖(f e)⁻¹ * b‖ₑ) a (nhds 0)

theorem tendsto_iff_enorm_neg_add_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖-f e + b‖ₑ) a (nhds 0)

theorem tendsto_one_iff_enorm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {f : α → E} {a : Filter α} : Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖ₑ) a (nhds 0)

theorem tendsto_zero_iff_enorm_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {f : α → E} {a : Filter α} : Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖ₑ) a (nhds 0)

@[simp]

theorem comap_norm_nhds_one {E : Type u_4} [SeminormedGroup E] : Filter.comap norm (nhds 0) = nhds 1

@[simp]

theorem comap_norm_nhds_zero {E : Type u_4} [SeminormedAddGroup E] : Filter.comap norm (nhds 0) = nhds 0

theorem squeeze_one_norm' {α : Type u_1} {E : Type u_4} [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.

theorem squeeze_zero_norm' {α : Type u_1} {E : Type u_4} [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.

theorem squeeze_one_norm {α : Type u_1} {E : Type u_4} [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.

theorem squeeze_zero_norm {α : Type u_1} {E : Type u_4} [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.

theorem tendsto_norm_inv_mul_self {E : Type u_4} [SeminormedGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a⁻¹ * x‖) (nhds x) (nhds 0)

theorem tendsto_norm_neg_add_self {E : Type u_4} [SeminormedAddGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖-a + x‖) (nhds x) (nhds 0)

theorem tendsto_norm_inv_mul_self_nhdsGE {E : Type u_4} [SeminormedGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a⁻¹ * x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))

theorem tendsto_norm_neg_add_self_nhdsGE {E : Type u_4} [SeminormedAddGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖-a + x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))

theorem tendsto_norm' {E : Type u_4} [SeminormedGroup E] {x : E} : Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)

theorem tendsto_norm {E : Type u_4} [SeminormedAddGroup E] {x : E} : Filter.Tendsto (fun (a : E) => ‖a‖) (nhds x) (nhds ‖x‖)

theorem tendsto_norm_one {E : Type u_4} [SeminormedGroup E] : Filter.Tendsto (fun (a : E) => ‖a‖) (nhds 1) (nhds 0)

See tendsto_norm_one for a version with pointed neighborhoods.

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

See tendsto_norm_zero for a version with pointed neighborhoods.

theorem continuous_norm' {E : Type u_4} [SeminormedGroup E] : Continuous fun (a : E) => ‖a‖

theorem continuous_norm {E : Type u_4} [SeminormedAddGroup E] : Continuous fun (a : E) => ‖a‖

theorem continuous_nnNorm' {E : Type u_4} [SeminormedGroup E] : Continuous fun (a : E) => ‖a‖₊

theorem continuous_nnNorm {E : Type u_4} [SeminormedAddGroup E] : Continuous fun (a : E) => ‖a‖₊

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

theorem continuous_nnnorm' {E : Type u_4} [SeminormedGroup E] : Continuous fun (a : E) => ‖a‖₊

Alias of continuous_nnNorm'.

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

theorem continuous_nnnorm {E : Type u_4} [SeminormedAddGroup E] : Continuous fun (a : E) => ‖a‖₊

Alias of continuous_nnNorm.

@[instance_reducible]

instance SeminormedGroup.toESeminormedMonoid {E : Type u_4} [SeminormedGroup E] : ESeminormedMonoid E

Equations

• SeminormedGroup.toESeminormedMonoid = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯, toMonoid := inst✝.toMonoid, enorm_zero := ⋯, enorm_mul_le := ⋯ }

@[instance_reducible]

instance SeminormedAddGroup.toESeminormedAddMonoid {E : Type u_4} [SeminormedAddGroup E] : ESeminormedAddMonoid E

Equations

• SeminormedAddGroup.toESeminormedAddMonoid = { toENorm := NNNorm.toENorm, continuous_enorm := ⋯, toAddMonoid := inst✝.toAddMonoid, enorm_zero := ⋯, enorm_add_le := ⋯ }

@[instance_reducible]

instance SeminormedCommGroup.toESeminormedCommMonoid {E : Type u_4} [SeminormedCommGroup E] : ESeminormedCommMonoid E

Equations

• SeminormedCommGroup.toESeminormedCommMonoid = { toESeminormedMonoid := SeminormedGroup.toESeminormedMonoid, mul_comm := ⋯ }

@[instance_reducible]

instance SeminormedAddCommGroup.toESeminormedAddCommMonoid {E : Type u_4} [SeminormedAddCommGroup E] : ESeminormedAddCommMonoid E

Equations

• SeminormedAddCommGroup.toESeminormedAddCommMonoid = { toESeminormedAddMonoid := SeminormedAddGroup.toESeminormedAddMonoid, add_comm := ⋯ }

@[instance_reducible]

instance NormedGroup.toENormedMonoid {F : Type u_7} [NormedGroup F] : ENormedMonoid F

Equations

• NormedGroup.toENormedMonoid = { toESeminormedMonoid := SeminormedGroup.toESeminormedMonoid, enorm_eq_zero := ⋯ }

@[instance_reducible]

instance NormedAddGroup.toENormedAddMonoid {F : Type u_7} [NormedAddGroup F] : ENormedAddMonoid F

Equations

• NormedAddGroup.toENormedAddMonoid = { toESeminormedAddMonoid := SeminormedAddGroup.toESeminormedAddMonoid, enorm_eq_zero := ⋯ }

@[instance_reducible]

instance NormedCommGroup.toENormedCommMonoid {E : Type u_4} [NormedCommGroup E] : ENormedCommMonoid E

Equations

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

@[instance_reducible]

instance NormedAddCommGroup.toENormedAddCommMonoid {E : Type u_4} [NormedAddCommGroup E] : ENormedAddCommMonoid E

Equations

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

theorem Inseparable.norm_eq_norm' {E : Type u_4} [SeminormedGroup E] {u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖

theorem Inseparable.norm_eq_norm {E : Type u_4} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖

theorem Inseparable.nnNorm_eq_nnNorm' {E : Type u_4} [SeminormedGroup E] {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊

theorem Inseparable.nnNorm_eq_nnNorm {E : Type u_4} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊

@[deprecated Inseparable.nnNorm_eq_nnNorm' (since := "2026-10-31")]

theorem Inseparable.nnnorm_eq_nnnorm' {E : Type u_4} [SeminormedGroup E] {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊

Alias of Inseparable.nnNorm_eq_nnNorm'.

@[deprecated Inseparable.nnNorm_eq_nnNorm (since := "2026-10-31")]

theorem Inseparable.nnnorm_eq_nnnorm {E : Type u_4} [SeminormedAddGroup E] {u v : E} (h : Inseparable u v) : ‖u‖₊ = ‖v‖₊

Alias of Inseparable.nnNorm_eq_nnNorm.

theorem Inseparable.enorm_eq_enorm {E : Type u_7} [TopologicalSpace E] [ContinuousENorm E] {u v : E} (h : Inseparable u v) : ‖u‖ₑ = ‖v‖ₑ

theorem mem_closure_one_iff_norm {E : Type u_4} [SeminormedGroup E] {x : E} : x ∈ closure {1} ↔ ‖x‖ = 0

theorem mem_closure_zero_iff_norm {E : Type u_4} [SeminormedAddGroup E] {x : E} : x ∈ closure {0} ↔ ‖x‖ = 0

theorem closure_one_eq {E : Type u_4} [SeminormedGroup E] : closure {1} = {x : E | ‖x‖ = 0}

theorem closure_zero_eq {E : Type u_4} [SeminormedAddGroup E] : closure {0} = {x : E | ‖x‖ = 0}

theorem Filter.Tendsto.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)

theorem Filter.Tendsto.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖) l (nhds ‖a‖)

theorem Filter.Tendsto.nnNorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

theorem Filter.Tendsto.nnNorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

@[deprecated Filter.Tendsto.nnNorm' (since := "2026-10-31")]

theorem Filter.Tendsto.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

Alias of Filter.Tendsto.nnNorm'.

@[deprecated Filter.Tendsto.nnNorm (since := "2026-10-31")]

theorem Filter.Tendsto.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖₊) l (nhds ‖a‖₊)

Alias of Filter.Tendsto.nnNorm.

theorem Continuous.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖

theorem Continuous.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖

theorem Continuous.nnNorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖₊

theorem Continuous.nnNorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖₊

@[deprecated Continuous.nnNorm' (since := "2026-10-31")]

theorem Continuous.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖₊

Alias of Continuous.nnNorm'.

@[deprecated Continuous.nnNorm (since := "2026-10-31")]

theorem Continuous.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖₊

Alias of Continuous.nnNorm.

theorem Filter.Tendsto.enorm {α : Type u_1} {E : Type u_4} [TopologicalSpace E] [ContinuousENorm E] {a : E} {l : Filter α} {f : α → E} (h : Tendsto f l (nhds a)) : Tendsto (fun (x : α) => ‖f x‖ₑ) l (nhds ‖a‖ₑ)

theorem ContinuousAt.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖) a

theorem ContinuousAt.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖) a

theorem ContinuousAt.nnNorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖₊) a

theorem ContinuousAt.nnNorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖₊) a

@[deprecated ContinuousAt.nnNorm' (since := "2026-10-31")]

theorem ContinuousAt.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖₊) a

Alias of ContinuousAt.nnNorm'.

@[deprecated ContinuousAt.nnNorm (since := "2026-10-31")]

theorem ContinuousAt.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {a : α} (h : ContinuousAt f a) : ContinuousAt (fun (x : α) => ‖f x‖₊) a

Alias of ContinuousAt.nnNorm.

theorem ContinuousWithinAt.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖) s a

theorem ContinuousWithinAt.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖) s a

theorem ContinuousWithinAt.nnNorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a

theorem ContinuousWithinAt.nnNorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a

@[deprecated ContinuousWithinAt.nnNorm' (since := "2026-10-31")]

theorem ContinuousWithinAt.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a

Alias of ContinuousWithinAt.nnNorm'.

@[deprecated ContinuousWithinAt.nnNorm (since := "2026-10-31")]

theorem ContinuousWithinAt.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a

Alias of ContinuousWithinAt.nnNorm.

theorem ContinuousOn.norm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖) s

theorem ContinuousOn.norm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖) s

theorem ContinuousOn.nnNorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖₊) s

theorem ContinuousOn.nnNorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖₊) s

@[deprecated ContinuousOn.nnNorm' (since := "2026-10-31")]

theorem ContinuousOn.nnnorm' {α : Type u_1} {E : Type u_4} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖₊) s

Alias of ContinuousOn.nnNorm'.

@[deprecated ContinuousOn.nnNorm (since := "2026-10-31")]

theorem ContinuousOn.nnnorm {α : Type u_1} {E : Type u_4} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} (h : ContinuousOn f s) : ContinuousOn (fun (x : α) => ‖f x‖₊) s

Alias of ContinuousOn.nnNorm.

theorem eventually_ne_of_tendsto_norm_atTop' {α : Type u_1} {E : Type u_4} [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.

theorem eventually_ne_of_tendsto_norm_atTop {α : Type u_1} {E : Type u_4} [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

theorem SeminormedGroup.mem_closure_iff {E : Type u_4} [SeminormedGroup E] {s : Set E} {a : E} : a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a⁻¹ * b‖ < ε

theorem SeminormedAddGroup.mem_closure_iff {E : Type u_4} [SeminormedAddGroup E] {s : Set E} {a : E} : a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖-a + b‖ < ε

theorem SeminormedGroup.tendstoUniformlyOn_one {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [SeminormedGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} : TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

theorem SeminormedAddGroup.tendstoUniformlyOn_zero {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [SeminormedAddGroup G] {f : ι → κ → G} {s : Set κ} {l : Filter ι} : TendstoUniformlyOn f 0 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

theorem SeminormedGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [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'

theorem SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [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'

theorem SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [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

theorem SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero {ι : Type u_2} {κ : Type u_3} {G : Type u_6} [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

theorem tendsto_iff_norm_div_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedCommGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e / b‖) a (nhds 0)

theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e - b‖) a (nhds 0)

theorem tendsto_iff_enorm_div_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedCommGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e / b‖ₑ) a (nhds 0)

theorem tendsto_iff_enorm_sub_tendsto_zero {α : Type u_1} {E : Type u_4} [SeminormedAddCommGroup E] {f : α → E} {a : Filter α} {b : E} : Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun (e : α) => ‖f e - b‖ₑ) a (nhds 0)

theorem SeminormedCommGroup.mem_closure_iff {E : Type u_4} [SeminormedCommGroup E] {a : E} {s : Set E} : a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε

theorem SeminormedAddCommGroup.mem_closure_iff {E : Type u_4} [SeminormedAddCommGroup E] {a : E} {s : Set E} : a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε

theorem tendsto_norm_div_self {E : Type u_4} [SeminormedCommGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhds 0)

theorem tendsto_norm_sub_self {E : Type u_4} [SeminormedAddCommGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhds 0)

theorem tendsto_norm_div_self_nhdsGE {E : Type u_4} [SeminormedCommGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a / x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))

theorem tendsto_norm_sub_self_nhdsGE {E : Type u_4} [SeminormedAddCommGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhdsWithin 0 (Set.Ici 0))

theorem controlled_prod_of_mem_closure {E : Type u_4} [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

theorem controlled_sum_of_mem_closure {E : Type u_4} [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

theorem controlled_prod_of_mem_closure_range {E : Type u_4} {F : Type u_5} [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

theorem controlled_sum_of_mem_closure_range {E : Type u_4} {F : Type u_5} [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

theorem tendsto_norm_nhdsNE_one {E : Type u_4} [NormedGroup E] : Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

See tendsto_norm_one for a version with full neighborhoods.

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

See tendsto_norm_zero for a version with full neighborhoods.

theorem tendsto_norm_inv_mul_self_nhdsNE {E : Type u_4} [NormedGroup E] (a : E) : Filter.Tendsto (fun (x : E) => ‖x⁻¹ * a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

theorem tendsto_norm_neg_add_self_nhdsNE {E : Type u_4} [NormedAddGroup E] (a : E) : Filter.Tendsto (fun (x : E) => ‖-x + a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

theorem comap_norm_nhdsGT_zero' (E : Type u_4) [NormedGroup E] : Filter.comap norm (nhdsWithin 0 (Set.Ioi 0)) = nhdsWithin 1 {1}ᶜ

In a normed group, the pullback under the norm of 𝓝[>] 0 is the punctured neighborhood of 1.

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

In a normed additive group, the pullback under the norm of 𝓝[>] 0 is the punctured neighborhood of 0.

theorem tendsto_norm_div_self_nhdsNE {E : Type u_7} [NormedCommGroup E] (a : E) : Filter.Tendsto (fun (x : E) => ‖x / a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))

theorem tendsto_norm_sub_self_nhdsNE {E : Type u_7} [NormedAddCommGroup E] (a : E) : Filter.Tendsto (fun (x : E) => ‖x - a‖) (nhdsWithin a {a}ᶜ) (nhdsWithin 0 (Set.Ioi 0))