Normed (semi)groups

In this file we define 10 classes:

• Norm, NNNorm: auxiliary classes endowing a type α with a function norm : α → ℝ (notation: ‖x‖) and nnnorm : α → ℝ≥0 (notation: ‖x‖₊), respectively;
• Seminormed...Group: A seminormed (additive) (commutative) group is an (additive) (commutative) group with a norm and a compatible pseudometric space structure: ∀ x y, dist x y = ‖x / y‖ or ∀ x y, dist x y = ‖x - y‖, depending on the group operation.
• Normed...Group: A normed (additive) (commutative) group is an (additive) (commutative) group with a norm and a compatible metric space structure.

We also prove basic properties of (semi)normed groups and provide some instances.

TODO

This file is huge; move material into separate files, such as Mathlib/Analysis/Normed/Group/Lemmas.lean.

Notes

The current convention dist x y = ‖x - y‖ means that the distance is invariant under right addition, but actions in mathlib are usually from the left. This means we might want to change it to dist x y = ‖-x + y‖.

The normed group hierarchy would lend itself well to a mixin design (that is, having SeminormedGroup and SeminormedAddGroup not extend Group and AddGroup), but we choose not to for performance concerns.

Tags

normed group

class Norm (E : Type u_8) : Type u_8

Auxiliary class, endowing a type E with a function norm : E → ℝ with notation ‖x‖. This class is designed to be extended in more interesting classes specifying the properties of the norm.

• norm : E → ℝ

  the ℝ-valued norm function.

class NNNorm (E : Type u_8) : Type u_8

Auxiliary class, endowing a type α with a function nnnorm : α → ℝ≥0 with notation ‖x‖₊.

• nnnorm : E → NNReal

  the ℝ≥0-valued norm function.

class ENorm (E : Type u_8) : Type u_8

Auxiliary class, endowing a type α with a function enorm : α → ℝ≥0∞ with notation ‖x‖ₑ.

• enorm : E → ENNReal

  the ℝ≥0∞-valued norm function.

def «term‖_‖» : Lean.ParserDescr

the ℝ-valued norm function.

Equations

• One or more equations did not get rendered due to their size.

def «term‖_‖₊» : Lean.ParserDescr

the ℝ≥0-valued norm function.

Equations

• One or more equations did not get rendered due to their size.

def «term‖_‖ₑ» : Lean.ParserDescr

the ℝ≥0∞-valued norm function.

Equations

• One or more equations did not get rendered due to their size.

class SeminormedAddGroup (E : Type u_8) extends Norm E, AddGroup E, PseudoMetricSpace E : Type u_8

A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

• norm : E → ℝ
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : E → E
• sub : E → E → E
• sub_eq_add_neg (a b : E) : a - b = a + -b
• zsmul : ℤ → E → E
• zsmul_zero' (a : E) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : E) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : E) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : E) : -a + a = 0
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : E) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

class SeminormedGroup (E : Type u_8) extends Norm E, Group E, PseudoMetricSpace E : Type u_8

A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

• norm : E → ℝ
• mul : E → E → E
• mul_assoc (a b c : E) : a * b * c = a * (b * c)
• one : E
• one_mul (a : E) : 1 * a = a
• mul_one (a : E) : a * 1 = a
• npow : ℕ → E → E
• npow_zero (x : E) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : E) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : E → E
• div : E → E → E
• div_eq_mul_inv (a b : E) : a / b = a * b⁻¹
• zpow : ℤ → E → E
• zpow_zero' (a : E) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : E) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : E) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : E) : a⁻¹ * a = 1
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : E) : dist x y = ‖x / y‖

  The distance function is induced by the norm.

class NormedAddGroup (E : Type u_8) extends Norm E, AddGroup E, MetricSpace E : Type u_8

A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

• norm : E → ℝ
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : E → E
• sub : E → E → E
• sub_eq_add_neg (a b : E) : a - b = a + -b
• zsmul : ℤ → E → E
• zsmul_zero' (a : E) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : E) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : E) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : E) : -a + a = 0
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : E} : dist x y = 0 → x = y
• dist_eq (x y : E) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

class NormedGroup (E : Type u_8) extends Norm E, Group E, MetricSpace E : Type u_8

A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

• norm : E → ℝ
• mul : E → E → E
• mul_assoc (a b c : E) : a * b * c = a * (b * c)
• one : E
• one_mul (a : E) : 1 * a = a
• mul_one (a : E) : a * 1 = a
• npow : ℕ → E → E
• npow_zero (x : E) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : E) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : E → E
• div : E → E → E
• div_eq_mul_inv (a b : E) : a / b = a * b⁻¹
• zpow : ℤ → E → E
• zpow_zero' (a : E) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : E) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : E) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : E) : a⁻¹ * a = 1
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : E} : dist x y = 0 → x = y
• dist_eq (x y : E) : dist x y = ‖x / y‖

  The distance function is induced by the norm.

class SeminormedAddCommGroup (E : Type u_8) extends Norm E, AddCommGroup E, PseudoMetricSpace E : Type u_8

A seminormed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a pseudometric space structure.

• norm : E → ℝ
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : E → E
• sub : E → E → E
• sub_eq_add_neg (a b : E) : a - b = a + -b
• zsmul : ℤ → E → E
• zsmul_zero' (a : E) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : E) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : E) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : E) : -a + a = 0
• add_comm (a b : E) : a + b = b + a
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : E) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

class SeminormedCommGroup (E : Type u_8) extends Norm E, CommGroup E, PseudoMetricSpace E : Type u_8

A seminormed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a pseudometric space structure.

• norm : E → ℝ
• mul : E → E → E
• mul_assoc (a b c : E) : a * b * c = a * (b * c)
• one : E
• one_mul (a : E) : 1 * a = a
• mul_one (a : E) : a * 1 = a
• npow : ℕ → E → E
• npow_zero (x : E) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : E) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : E → E
• div : E → E → E
• div_eq_mul_inv (a b : E) : a / b = a * b⁻¹
• zpow : ℤ → E → E
• zpow_zero' (a : E) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : E) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : E) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : E) : a⁻¹ * a = 1
• mul_comm (a b : E) : a * b = b * a
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• dist_eq (x y : E) : dist x y = ‖x / y‖

  The distance function is induced by the norm.

class NormedAddCommGroup (E : Type u_8) extends Norm E, AddCommGroup E, MetricSpace E : Type u_8

A normed group is an additive group endowed with a norm for which dist x y = ‖x - y‖ defines a metric space structure.

• norm : E → ℝ
• add : E → E → E
• add_assoc (a b c : E) : a + b + c = a + (b + c)
• zero : E
• zero_add (a : E) : 0 + a = a
• add_zero (a : E) : a + 0 = a
• nsmul : ℕ → E → E
• nsmul_zero (x : E) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : E) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : E → E
• sub : E → E → E
• sub_eq_add_neg (a b : E) : a - b = a + -b
• zsmul : ℤ → E → E
• zsmul_zero' (a : E) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : E) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : E) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : E) : -a + a = 0
• add_comm (a b : E) : a + b = b + a
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : E} : dist x y = 0 → x = y
• dist_eq (x y : E) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

class NormedCommGroup (E : Type u_8) extends Norm E, CommGroup E, MetricSpace E : Type u_8

A normed group is a group endowed with a norm for which dist x y = ‖x / y‖ defines a metric space structure.

• norm : E → ℝ
• mul : E → E → E
• mul_assoc (a b c : E) : a * b * c = a * (b * c)
• one : E
• one_mul (a : E) : 1 * a = a
• mul_one (a : E) : a * 1 = a
• npow : ℕ → E → E
• npow_zero (x : E) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : E) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : E → E
• div : E → E → E
• div_eq_mul_inv (a b : E) : a / b = a * b⁻¹
• zpow : ℤ → E → E
• zpow_zero' (a : E) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : E) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : E) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : E) : a⁻¹ * a = 1
• mul_comm (a b : E) : a * b = b * a
• dist : E → E → ℝ
• dist_self (x : E) : dist x x = 0
• dist_comm (x y : E) : dist x y = dist y x
• dist_triangle (x y z : E) : dist x z ≤ dist x y + dist y z
• edist : E → E → ENNReal
• edist_dist (x y : E) : PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace E
• uniformity_dist : uniformity E = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : E × E | dist p.1 p.2 < ε}
• toBornology : Bornology E
• cobounded_sets : (Bornology.cobounded E).sets = {s : Set E | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : E} : dist x y = 0 → x = y
• dist_eq (x y : E) : dist x y = ‖x / y‖

  The distance function is induced by the norm.

@[instance 100]

instance NormedGroup.toSeminormedGroup {E : Type u_5} [NormedGroup E] : SeminormedGroup E

Equations

• NormedGroup.toSeminormedGroup = SeminormedGroup.mk ⋯

@[instance 100]

instance NormedAddGroup.toSeminormedAddGroup {E : Type u_5} [NormedAddGroup E] : SeminormedAddGroup E

Equations

• NormedAddGroup.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯

@[instance 100]

instance NormedCommGroup.toSeminormedCommGroup {E : Type u_5} [NormedCommGroup E] : SeminormedCommGroup E

Equations

• NormedCommGroup.toSeminormedCommGroup = SeminormedCommGroup.mk ⋯

@[instance 100]

instance NormedAddCommGroup.toSeminormedAddCommGroup {E : Type u_5} [NormedAddCommGroup E] : SeminormedAddCommGroup E

Equations

• NormedAddCommGroup.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

@[instance 100]

instance SeminormedCommGroup.toSeminormedGroup {E : Type u_5} [SeminormedCommGroup E] : SeminormedGroup E

Equations

• SeminormedCommGroup.toSeminormedGroup = SeminormedGroup.mk ⋯

@[instance 100]

instance SeminormedAddCommGroup.toSeminormedAddGroup {E : Type u_5} [SeminormedAddCommGroup E] : SeminormedAddGroup E

Equations

• SeminormedAddCommGroup.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯

@[instance 100]

instance NormedCommGroup.toNormedGroup {E : Type u_5} [NormedCommGroup E] : NormedGroup E

Equations

• NormedCommGroup.toNormedGroup = NormedGroup.mk ⋯

@[instance 100]

instance NormedAddCommGroup.toNormedAddGroup {E : Type u_5} [NormedAddCommGroup E] : NormedAddGroup E

Equations

• NormedAddCommGroup.toNormedAddGroup = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev NormedGroup.ofSeparation {E : Type u_5} [SeminormedGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1) : NormedGroup E

Construct a NormedGroup from a SeminormedGroup satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedGroup instance as a special case of a more general SeminormedGroup instance.

Equations

• NormedGroup.ofSeparation h = NormedGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddGroup.ofSeparation {E : Type u_5} [SeminormedAddGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) : NormedAddGroup E

Construct a NormedAddGroup from a SeminormedAddGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddGroup instance as a special case of a more general SeminormedAddGroup instance.

Equations

• NormedAddGroup.ofSeparation h = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev NormedCommGroup.ofSeparation {E : Type u_5} [SeminormedCommGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 1) : NormedCommGroup E

Construct a NormedCommGroup from a SeminormedCommGroup satisfying ∀ x, ‖x‖ = 0 → x = 1. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedCommGroup instance as a special case of a more general SeminormedCommGroup instance.

Equations

• NormedCommGroup.ofSeparation h = NormedCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddCommGroup.ofSeparation {E : Type u_5} [SeminormedAddCommGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) : NormedAddCommGroup E

Construct a NormedAddCommGroup from a SeminormedAddCommGroup satisfying ∀ x, ‖x‖ = 0 → x = 0. This avoids having to go back to the (Pseudo)MetricSpace level when declaring a NormedAddCommGroup instance as a special case of a more general SeminormedAddCommGroup instance.

Equations

• NormedAddCommGroup.ofSeparation h = NormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedGroup.ofMulDist {E : Type u_5} [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x * z) (y * z)) : SeminormedGroup E

Construct a seminormed group from a multiplication-invariant distance.

Equations

• SeminormedGroup.ofMulDist h₁ h₂ = SeminormedGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddGroup.ofAddDist {E : Type u_5} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) : SeminormedAddGroup E

Construct a seminormed group from a translation-invariant distance.

Equations

• SeminormedAddGroup.ofAddDist h₁ h₂ = SeminormedAddGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedGroup.ofMulDist' {E : Type u_5} [Norm E] [Group E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) ≤ dist x y) : SeminormedGroup E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations

• SeminormedGroup.ofMulDist' h₁ h₂ = SeminormedGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddGroup.ofAddDist' {E : Type u_5} [Norm E] [AddGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y) : SeminormedAddGroup E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations

• SeminormedAddGroup.ofAddDist' h₁ h₂ = SeminormedAddGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedCommGroup.ofMulDist {E : Type u_5} [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x * z) (y * z)) : SeminormedCommGroup E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations

• SeminormedCommGroup.ofMulDist h₁ h₂ = SeminormedCommGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofAddDist {E : Type u_5} [Norm E] [AddCommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) : SeminormedAddCommGroup E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations

• SeminormedAddCommGroup.ofAddDist h₁ h₂ = SeminormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedCommGroup.ofMulDist' {E : Type u_5} [Norm E] [CommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) ≤ dist x y) : SeminormedCommGroup E

Construct a seminormed group from a multiplication-invariant pseudodistance.

Equations

• SeminormedCommGroup.ofMulDist' h₁ h₂ = SeminormedCommGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddCommGroup.ofAddDist' {E : Type u_5} [Norm E] [AddCommGroup E] [PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y) : SeminormedAddCommGroup E

Construct a seminormed group from a translation-invariant pseudodistance.

Equations

• SeminormedAddCommGroup.ofAddDist' h₁ h₂ = SeminormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedGroup.ofMulDist {E : Type u_5} [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x * z) (y * z)) : NormedGroup E

Construct a normed group from a multiplication-invariant distance.

Equations

• NormedGroup.ofMulDist h₁ h₂ = NormedGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddGroup.ofAddDist {E : Type u_5} [Norm E] [AddGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) : NormedAddGroup E

Construct a normed group from a translation-invariant distance.

Equations

• NormedAddGroup.ofAddDist h₁ h₂ = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev NormedGroup.ofMulDist' {E : Type u_5} [Norm E] [Group E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) ≤ dist x y) : NormedGroup E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations

• NormedGroup.ofMulDist' h₁ h₂ = NormedGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddGroup.ofAddDist' {E : Type u_5} [Norm E] [AddGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y) : NormedAddGroup E

Construct a normed group from a translation-invariant pseudodistance.

Equations

• NormedAddGroup.ofAddDist' h₁ h₂ = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev NormedCommGroup.ofMulDist {E : Type u_5} [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x * z) (y * z)) : NormedCommGroup E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations

• NormedCommGroup.ofMulDist h₁ h₂ = NormedCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddCommGroup.ofAddDist {E : Type u_5} [Norm E] [AddCommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist x y ≤ dist (x + z) (y + z)) : NormedAddCommGroup E

Construct a normed group from a translation-invariant pseudodistance.

Equations

• NormedAddCommGroup.ofAddDist h₁ h₂ = NormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedCommGroup.ofMulDist' {E : Type u_5} [Norm E] [CommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 1) (h₂ : ∀ (x y z : E), dist (x * z) (y * z) ≤ dist x y) : NormedCommGroup E

Construct a normed group from a multiplication-invariant pseudodistance.

Equations

• NormedCommGroup.ofMulDist' h₁ h₂ = NormedCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddCommGroup.ofAddDist' {E : Type u_5} [Norm E] [AddCommGroup E] [MetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist x 0) (h₂ : ∀ (x y z : E), dist (x + z) (y + z) ≤ dist x y) : NormedAddCommGroup E

Construct a normed group from a translation-invariant pseudodistance.

Equations

• NormedAddCommGroup.ofAddDist' h₁ h₂ = NormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev GroupSeminorm.toSeminormedGroup {E : Type u_5} [Group E] (f : GroupSeminorm E) : SeminormedGroup E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toSeminormedGroup = SeminormedGroup.mk ⋯

@[reducible, inline]

abbrev AddGroupSeminorm.toSeminormedAddGroup {E : Type u_5} [AddGroup E] (f : AddGroupSeminorm E) : SeminormedAddGroup E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toSeminormedAddGroup = SeminormedAddGroup.mk ⋯

@[reducible, inline]

abbrev GroupSeminorm.toSeminormedCommGroup {E : Type u_5} [CommGroup E] (f : GroupSeminorm E) : SeminormedCommGroup E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toSeminormedCommGroup = SeminormedCommGroup.mk ⋯

@[reducible, inline]

abbrev AddGroupSeminorm.toSeminormedAddCommGroup {E : Type u_5} [AddCommGroup E] (f : AddGroupSeminorm E) : SeminormedAddCommGroup E

Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the pseudometric space structure from the seminorm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev GroupNorm.toNormedGroup {E : Type u_5} [Group E] (f : GroupNorm E) : NormedGroup E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toNormedGroup = NormedGroup.mk ⋯

@[reducible, inline]

abbrev AddGroupNorm.toNormedAddGroup {E : Type u_5} [AddGroup E] (f : AddGroupNorm E) : NormedAddGroup E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toNormedAddGroup = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev GroupNorm.toNormedCommGroup {E : Type u_5} [CommGroup E] (f : GroupNorm E) : NormedCommGroup E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toNormedCommGroup = NormedCommGroup.mk ⋯

@[reducible, inline]

abbrev AddGroupNorm.toNormedAddCommGroup {E : Type u_5} [AddCommGroup E] (f : AddGroupNorm E) : NormedAddCommGroup E

Construct a normed group from a norm, i.e., registering the distance and the metric space structure from the norm properties. Note that in most cases this instance creates bad definitional equalities (e.g., it does not take into account a possibly existing UniformSpace instance on E).

Equations

• f.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯

theorem dist_eq_norm_div {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b = ‖a / b‖

theorem dist_eq_norm_sub {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖a - b‖

theorem dist_eq_norm_div' {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b = ‖b / a‖

theorem dist_eq_norm_sub' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖b - a‖

theorem dist_eq_norm {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖a - b‖

Alias of dist_eq_norm_sub.

theorem dist_eq_norm' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b = ‖b - a‖

Alias of dist_eq_norm_sub'.

theorem DiscreteTopology.of_forall_le_norm' {E : Type u_5} [SeminormedGroup E] {r : ℝ} (hpos : 0 < r) (hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖) : DiscreteTopology E

theorem DiscreteTopology.of_forall_le_norm {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (hpos : 0 < r) (hr : ∀ (x : E), x ≠ 0 → r ≤ ‖x‖) : DiscreteTopology E

@[simp]

theorem dist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : dist a 1 = ‖a‖

@[simp]

theorem dist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : dist a 0 = ‖a‖

theorem inseparable_one_iff_norm {E : Type u_5} [SeminormedGroup E] {a : E} : Inseparable a 1 ↔ ‖a‖ = 0

theorem inseparable_zero_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a : E} : Inseparable a 0 ↔ ‖a‖ = 0

@[simp]

theorem dist_one_left {E : Type u_5} [SeminormedGroup E] : dist 1 = norm

@[simp]

theorem dist_zero_left {E : Type u_5} [SeminormedAddGroup E] : dist 0 = norm

theorem norm_div_rev {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖ = ‖b / a‖

theorem norm_sub_rev {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ = ‖b - a‖

@[simp]

theorem norm_inv' {E : Type u_5} [SeminormedGroup E] (a : E) : ‖a⁻¹‖ = ‖a‖

@[simp]

theorem norm_neg {E : Type u_5} [SeminormedAddGroup E] (a : E) : ‖-a‖ = ‖a‖

@[simp]

theorem norm_zpow_abs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ |n|‖ = ‖a ^ n‖

@[simp]

theorem norm_abs_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖|n| • a‖ = ‖n • a‖

@[simp]

theorem norm_pow_natAbs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ n.natAbs‖ = ‖a ^ n‖

@[simp]

theorem norm_natAbs_smul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖n.natAbs • a‖ = ‖n • a‖

theorem norm_zpow_isUnit {E : Type u_5} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖ = ‖a‖

theorem norm_isUnit_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖n • a‖ = ‖a‖

@[simp]

theorem norm_units_zsmul {E : Type u_8} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖ = ‖a‖

theorem dist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : dist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖

theorem dist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : dist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖

theorem norm_mul_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a * b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_add_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a + b‖ ≤ ‖a‖ + ‖b‖

Triangle inequality for the norm.

theorem norm_mul_le_of_le' {E : Type u_5} [SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ * a₂‖ ≤ r₁ + r₂

Triangle inequality for the norm.

theorem norm_add_le_of_le {E : Type u_5} [SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (h₁ : ‖a₁‖ ≤ r₁) (h₂ : ‖a₂‖ ≤ r₂) : ‖a₁ + a₂‖ ≤ r₁ + r₂

Triangle inequality for the norm.

theorem norm_mul₃_le' {E : Type u_5} [SeminormedGroup E] {a b c : E} : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_add₃_le {E : Type u_5} [SeminormedAddGroup E] {a b c : E} : ‖a + b + c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

Triangle inequality for the norm.

theorem norm_div_le_norm_div_add_norm_div {E : Type u_5} [SeminormedGroup E] (a b c : E) : ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖

theorem norm_sub_le_norm_sub_add_norm_sub {E : Type u_5} [SeminormedAddGroup E] (a b c : E) : ‖a - c‖ ≤ ‖a - b‖ + ‖b - c‖

@[simp]

theorem norm_nonneg' {E : Type u_5} [SeminormedGroup E] (a : E) : 0 ≤ ‖a‖

@[simp]

theorem norm_nonneg {E : Type u_5} [SeminormedAddGroup E] (a : E) : 0 ≤ ‖a‖

@[simp]

theorem abs_norm' {E : Type u_5} [SeminormedGroup E] (z : E) : |‖z‖| = ‖z‖

@[simp]

theorem abs_norm {E : Type u_5} [SeminormedAddGroup E] (z : E) : |‖z‖| = ‖z‖

@[simp]

theorem norm_one' {E : Type u_5} [SeminormedGroup E] : ‖1‖ = 0

@[simp]

theorem norm_zero {E : Type u_5} [SeminormedAddGroup E] : ‖0‖ = 0

theorem ne_one_of_norm_ne_zero {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖ ≠ 0 → a ≠ 1

theorem ne_zero_of_norm_ne_zero {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖ ≠ 0 → a ≠ 0

theorem norm_of_subsingleton' {E : Type u_5} [SeminormedGroup E] [Subsingleton E] (a : E) : ‖a‖ = 0

theorem norm_of_subsingleton {E : Type u_5} [SeminormedAddGroup E] [Subsingleton E] (a : E) : ‖a‖ = 0

theorem zero_lt_one_add_norm_sq' {E : Type u_5} [SeminormedGroup E] (x : E) : 0 < 1 + ‖x‖ ^ 2

theorem zero_lt_one_add_norm_sq {E : Type u_5} [SeminormedAddGroup E] (x : E) : 0 < 1 + ‖x‖ ^ 2

theorem norm_div_le {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖ ≤ ‖a‖ + ‖b‖

theorem norm_sub_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖ ≤ ‖a‖ + ‖b‖

theorem norm_div_le_of_le {E : Type u_5} [SeminormedGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ / a₂‖ ≤ r₁ + r₂

theorem norm_sub_le_of_le {E : Type u_5} [SeminormedAddGroup E] {a₁ a₂ : E} {r₁ r₂ : ℝ} (H₁ : ‖a₁‖ ≤ r₁) (H₂ : ‖a₂‖ ≤ r₂) : ‖a₁ - a₂‖ ≤ r₁ + r₂

theorem dist_le_norm_add_norm' {E : Type u_5} [SeminormedGroup E] (a b : E) : dist a b ≤ ‖a‖ + ‖b‖

theorem dist_le_norm_add_norm {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist a b ≤ ‖a‖ + ‖b‖

theorem abs_norm_sub_norm_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a / b‖

theorem abs_norm_sub_norm_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : |‖a‖ - ‖b‖| ≤ ‖a - b‖

theorem norm_sub_norm_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a / b‖

theorem norm_sub_norm_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖ - ‖b‖ ≤ ‖a - b‖

theorem dist_norm_norm_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a / b‖

theorem dist_norm_norm_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : dist ‖a‖ ‖b‖ ≤ ‖a - b‖

theorem norm_le_norm_add_norm_div' {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u - v‖

theorem norm_le_norm_add_norm_div {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u / v‖

theorem norm_le_norm_add_norm_sub {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u - v‖

theorem norm_le_insert' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖v‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub'.

theorem norm_le_insert {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u - v‖

Alias of norm_le_norm_add_norm_sub.

theorem norm_le_mul_norm_add {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖u‖ ≤ ‖u * v‖ + ‖v‖

theorem norm_le_add_norm_add {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖u‖ ≤ ‖u + v‖ + ‖v‖

theorem norm_le_mul_norm_add' {E : Type u_5} [SeminormedGroup E] (u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖

An analogue of norm_le_mul_norm_add for the multiplication from the left.

theorem norm_le_add_norm_add' {E : Type u_5} [SeminormedAddGroup E] (u v : E) : ‖v‖ ≤ ‖u + v‖ + ‖u‖

An analogue of norm_le_add_norm_add for the addition from the left.

theorem norm_mul_eq_norm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x * y‖ = ‖y‖

theorem norm_add_eq_norm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x + y‖ = ‖y‖

theorem norm_mul_eq_norm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x * y‖ = ‖x‖

theorem norm_add_eq_norm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x + y‖ = ‖x‖

theorem norm_div_eq_norm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x / y‖ = ‖y‖

theorem norm_sub_eq_norm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖ = 0) : ‖x - y‖ = ‖y‖

theorem norm_div_eq_norm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x / y‖ = ‖x‖

theorem norm_sub_eq_norm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖ = 0) : ‖x - y‖ = ‖x‖

theorem ball_eq' {E : Type u_5} [SeminormedGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖x / y‖ < ε}

theorem ball_eq {E : Type u_5} [SeminormedAddGroup E] (y : E) (ε : ℝ) : Metric.ball y ε = {x : E | ‖x - y‖ < ε}

theorem ball_one_eq {E : Type u_5} [SeminormedGroup E] (r : ℝ) : Metric.ball 1 r = {x : E | ‖x‖ < r}

theorem ball_zero_eq {E : Type u_5} [SeminormedAddGroup E] (r : ℝ) : Metric.ball 0 r = {x : E | ‖x‖ < r}

theorem mem_ball_iff_norm'' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b / a‖ < r

theorem mem_ball_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖b - a‖ < r

theorem mem_ball_iff_norm''' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a / b‖ < r

theorem mem_ball_iff_norm' {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.ball a r ↔ ‖a - b‖ < r

theorem mem_ball_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 1 r ↔ ‖a‖ < r

theorem mem_ball_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.ball 0 r ↔ ‖a‖ < r

theorem mem_closedBall_iff_norm'' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b / a‖ ≤ r

theorem mem_closedBall_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖b - a‖ ≤ r

theorem mem_closedBall_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 1 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.closedBall 0 r ↔ ‖a‖ ≤ r

theorem mem_closedBall_iff_norm''' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a / b‖ ≤ r

theorem mem_closedBall_iff_norm' {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.closedBall a r ↔ ‖a - b‖ ≤ r

theorem norm_le_of_mem_closedBall' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r

theorem norm_le_of_mem_closedBall {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.closedBall a r) : ‖b‖ ≤ ‖a‖ + r

theorem norm_le_norm_add_const_of_dist_le' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

theorem norm_le_norm_add_const_of_dist_le {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : dist a b ≤ r → ‖a‖ ≤ ‖b‖ + r

theorem norm_lt_of_mem_ball' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r

theorem norm_lt_of_mem_ball {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} (h : b ∈ Metric.ball a r) : ‖b‖ < ‖a‖ + r

theorem norm_div_sub_norm_div_le_norm_div {E : Type u_5} [SeminormedGroup E] (u v w : E) : ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖

theorem norm_sub_sub_norm_sub_le_norm_sub {E : Type u_5} [SeminormedAddGroup E] (u v w : E) : ‖u - w‖ - ‖v - w‖ ≤ ‖u - v‖

@[simp]

theorem mem_sphere_iff_norm' {E : Type u_5} [SeminormedGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b / a‖ = r

@[simp]

theorem mem_sphere_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a b : E} {r : ℝ} : b ∈ Metric.sphere a r ↔ ‖b - a‖ = r

theorem mem_sphere_one_iff_norm {E : Type u_5} [SeminormedGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 1 r ↔ ‖a‖ = r

theorem mem_sphere_zero_iff_norm {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ℝ} : a ∈ Metric.sphere 0 r ↔ ‖a‖ = r

@[simp]

theorem norm_eq_of_mem_sphere' {E : Type u_5} [SeminormedGroup E] {r : ℝ} (x : ↑(Metric.sphere 1 r)) : ‖↑x‖ = r

@[simp]

theorem norm_eq_of_mem_sphere {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (x : ↑(Metric.sphere 0 r)) : ‖↑x‖ = r

theorem ne_one_of_mem_sphere {E : Type u_5} [SeminormedGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 1 r)) : ↑x ≠ 1

theorem ne_zero_of_mem_sphere {E : Type u_5} [SeminormedAddGroup E] {r : ℝ} (hr : r ≠ 0) (x : ↑(Metric.sphere 0 r)) : ↑x ≠ 0

theorem ne_one_of_mem_unit_sphere {E : Type u_5} [SeminormedGroup E] (x : ↑(Metric.sphere 1 1)) : ↑x ≠ 1

theorem ne_zero_of_mem_unit_sphere {E : Type u_5} [SeminormedAddGroup E] (x : ↑(Metric.sphere 0 1)) : ↑x ≠ 0

def normGroupSeminorm (E : Type u_5) [SeminormedGroup E] : GroupSeminorm E

The norm of a seminormed group as a group seminorm.

Equations

• normGroupSeminorm E = { toFun := norm, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }

def normAddGroupSeminorm (E : Type u_5) [SeminormedAddGroup E] : AddGroupSeminorm E

The norm of a seminormed group as an additive group seminorm.

Equations

• normAddGroupSeminorm E = { toFun := norm, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ }

@[simp]

theorem coe_normGroupSeminorm (E : Type u_5) [SeminormedGroup E] : ⇑(normGroupSeminorm E) = norm

@[simp]

theorem coe_normAddGroupSeminorm (E : Type u_5) [SeminormedAddGroup E] : ⇑(normAddGroupSeminorm E) = norm

theorem NormedCommGroup.tendsto_nhds_one {α : Type u_2} {E : Type u_5} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 1) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

theorem NormedAddCommGroup.tendsto_nhds_zero {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

theorem NormedCommGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' / x‖ < δ → ‖f x' / y‖ < ε

theorem NormedAddCommGroup.tendsto_nhds_nhds {E : Type u_5} {F : Type u_6} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {x : E} {y : F} : Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖x' - x‖ < δ → ‖f x' - y‖ < ε

theorem NormedCommGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y / x‖ < ε}

theorem NormedAddCommGroup.nhds_basis_norm_lt {E : Type u_5} [SeminormedAddGroup E] (x : E) : (nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y - x‖ < ε}

theorem NormedCommGroup.nhds_one_basis_norm_lt {E : Type u_5} [SeminormedGroup E] : (nhds 1).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

theorem NormedAddCommGroup.nhds_zero_basis_norm_lt {E : Type u_5} [SeminormedAddGroup E] : (nhds 0).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {y : E | ‖y‖ < ε}

theorem NormedCommGroup.uniformity_basis_dist {E : Type u_5} [SeminormedGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 / p.2‖ < ε}

theorem NormedAddCommGroup.uniformity_basis_dist {E : Type u_5} [SeminormedAddGroup E] : (uniformity E).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : E × E | ‖p.1 - p.2‖ < ε}

@[instance 100]

instance SeminormedGroup.toNNNorm {E : Type u_5} [SeminormedGroup E] : NNNorm E

Equations

• SeminormedGroup.toNNNorm = { nnnorm := fun (a : E) => ⟨‖a‖, ⋯⟩ }

@[instance 100]

instance SeminormedAddGroup.toNNNorm {E : Type u_5} [SeminormedAddGroup E] : NNNorm E

Equations

• SeminormedAddGroup.toNNNorm = { nnnorm := fun (a : E) => ⟨‖a‖, ⋯⟩ }

@[simp]

theorem coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (a : E) : ↑‖a‖₊ = ‖a‖

@[simp]

theorem coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : ↑‖a‖₊ = ‖a‖

@[simp]

theorem coe_comp_nnnorm' {E : Type u_5} [SeminormedGroup E] : NNReal.toReal ∘ nnnorm = norm

@[simp]

theorem coe_comp_nnnorm {E : Type u_5} [SeminormedAddGroup E] : NNReal.toReal ∘ nnnorm = norm

theorem norm_toNNReal' {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖.toNNReal = ‖a‖₊

theorem norm_toNNReal {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖.toNNReal = ‖a‖₊

theorem nndist_eq_nnnorm_div {E : Type u_5} [SeminormedGroup E] (a b : E) : nndist a b = ‖a / b‖₊

theorem nndist_eq_nnnorm_sub {E : Type u_5} [SeminormedAddGroup E] (a b : E) : nndist a b = ‖a - b‖₊

theorem nndist_eq_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a b : E) : nndist a b = ‖a - b‖₊

Alias of nndist_eq_nnnorm_sub.

@[simp]

theorem nndist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : nndist a 1 = ‖a‖₊

@[simp]

theorem nndist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : nndist a 0 = ‖a‖₊

@[simp]

theorem edist_one_right {E : Type u_5} [SeminormedGroup E] (a : E) : edist a 1 = ↑‖a‖₊

@[simp]

theorem edist_zero_right {E : Type u_5} [SeminormedAddGroup E] (a : E) : edist a 0 = ↑‖a‖₊

@[simp]

theorem nnnorm_one' {E : Type u_5} [SeminormedGroup E] : ‖1‖₊ = 0

@[simp]

theorem nnnorm_zero {E : Type u_5} [SeminormedAddGroup E] : ‖0‖₊ = 0

theorem ne_one_of_nnnorm_ne_zero {E : Type u_5} [SeminormedGroup E] {a : E} : ‖a‖₊ ≠ 0 → a ≠ 1

theorem ne_zero_of_nnnorm_ne_zero {E : Type u_5} [SeminormedAddGroup E] {a : E} : ‖a‖₊ ≠ 0 → a ≠ 0

theorem nnnorm_mul_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnnorm_add_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a + b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem norm_pow_le_mul_norm {E : Type u_5} [SeminormedGroup E] {a : E} {n : ℕ} : ‖a ^ n‖ ≤ ↑n * ‖a‖

theorem norm_nsmul_le {E : Type u_5} [SeminormedAddGroup E] {a : E} {n : ℕ} : ‖n • a‖ ≤ ↑n * ‖a‖

theorem nnnorm_pow_le_mul_norm {E : Type u_5} [SeminormedGroup E] {a : E} {n : ℕ} : ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

theorem nnnorm_nsmul_le {E : Type u_5} [SeminormedAddGroup E] {a : E} {n : ℕ} : ‖n • a‖₊ ≤ ↑n * ‖a‖₊

@[simp]

theorem nnnorm_inv' {E : Type u_5} [SeminormedGroup E] (a : E) : ‖a⁻¹‖₊ = ‖a‖₊

@[simp]

theorem nnnorm_neg {E : Type u_5} [SeminormedAddGroup E] (a : E) : ‖-a‖₊ = ‖a‖₊

@[simp]

theorem nnnorm_zpow_abs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ |n|‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnnorm_abs_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖|n| • a‖₊ = ‖n • a‖₊

@[simp]

theorem nnnorm_pow_natAbs {E : Type u_5} [SeminormedGroup E] (a : E) (n : ℤ) : ‖a ^ n.natAbs‖₊ = ‖a ^ n‖₊

@[simp]

theorem nnnorm_natAbs_smul {E : Type u_5} [SeminormedAddGroup E] (a : E) (n : ℤ) : ‖n.natAbs • a‖₊ = ‖n • a‖₊

theorem nnnorm_zpow_isUnit {E : Type u_5} [SeminormedGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖a ^ n‖₊ = ‖a‖₊

theorem nnnorm_isUnit_zsmul {E : Type u_5} [SeminormedAddGroup E] (a : E) {n : ℤ} (hn : IsUnit n) : ‖n • a‖₊ = ‖a‖₊

@[simp]

theorem nnnorm_units_zsmul {E : Type u_8} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖₊ = ‖a‖₊

@[simp]

theorem nndist_one_left {E : Type u_5} [SeminormedGroup E] (a : E) : nndist 1 a = ‖a‖₊

@[simp]

theorem nndist_zero_left {E : Type u_5} [SeminormedAddGroup E] (a : E) : nndist 0 a = ‖a‖₊

@[simp]

theorem edist_one_left {E : Type u_5} [SeminormedGroup E] (a : E) : edist 1 a = ↑‖a‖₊

@[simp]

theorem edist_zero_left {E : Type u_5} [SeminormedAddGroup E] (a : E) : edist 0 a = ↑‖a‖₊

theorem nndist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : nndist (s.mulIndicator f x) (t.mulIndicator f x) = ‖(symmDiff s t).mulIndicator f x‖₊

theorem nndist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : nndist (s.indicator f x) (t.indicator f x) = ‖(symmDiff s t).indicator f x‖₊

theorem nnnorm_div_le {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a / b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nnnorm_sub_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊

theorem nndist_nnnorm_nnnorm_le' {E : Type u_5} [SeminormedGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a / b‖₊

theorem nndist_nnnorm_nnnorm_le {E : Type u_5} [SeminormedAddGroup E] (a b : E) : nndist ‖a‖₊ ‖b‖₊ ≤ ‖a - b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_div {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_sub {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_div' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a / b‖₊

theorem nnnorm_le_nnnorm_add_nnnorm_sub' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊

theorem nnnorm_le_insert' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖b‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

theorem nnnorm_le_insert {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a‖₊ + ‖a - b‖₊

Alias of nnnorm_le_nnnorm_add_nnnorm_sub.

theorem nnnorm_le_mul_nnnorm_add {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖a‖₊ ≤ ‖a * b‖₊ + ‖b‖₊

theorem nnnorm_le_add_nnnorm_add {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖a‖₊ ≤ ‖a + b‖₊ + ‖b‖₊

theorem nnnorm_le_mul_nnnorm_add' {E : Type u_5} [SeminormedGroup E] (a b : E) : ‖b‖₊ ≤ ‖a * b‖₊ + ‖a‖₊

An analogue of nnnorm_le_mul_nnnorm_add for the multiplication from the left.

theorem nnnorm_le_add_nnnorm_add' {E : Type u_5} [SeminormedAddGroup E] (a b : E) : ‖b‖₊ ≤ ‖a + b‖₊ + ‖a‖₊

An analogue of nnnorm_le_add_nnnorm_add for the addition from the left.

theorem nnnorm_mul_eq_nnnorm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x * y‖₊ = ‖y‖₊

theorem nnnorm_add_eq_nnnorm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x + y‖₊ = ‖y‖₊

theorem nnnorm_mul_eq_nnnorm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x * y‖₊ = ‖x‖₊

theorem nnnorm_add_eq_nnnorm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x + y‖₊ = ‖x‖₊

theorem nnnorm_div_eq_nnnorm_right {E : Type u_5} [SeminormedGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x / y‖₊ = ‖y‖₊

theorem nnnorm_sub_eq_nnnorm_right {E : Type u_5} [SeminormedAddGroup E] {x : E} (y : E) (h : ‖x‖₊ = 0) : ‖x - y‖₊ = ‖y‖₊

theorem nnnorm_div_eq_nnnorm_left {E : Type u_5} [SeminormedGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x / y‖₊ = ‖x‖₊

theorem nnnorm_sub_eq_nnnorm_left {E : Type u_5} [SeminormedAddGroup E] (x : E) {y : E} (h : ‖y‖₊ = 0) : ‖x - y‖₊ = ‖x‖₊

theorem ofReal_norm_eq_coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (a : E) : ENNReal.ofReal ‖a‖ = ↑‖a‖₊

theorem ofReal_norm_eq_coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : ENNReal.ofReal ‖a‖ = ↑‖a‖₊

theorem toReal_coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (a : E) : (↑‖a‖₊).toReal = ‖a‖

The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem toReal_coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (a : E) : (↑‖a‖₊).toReal = ‖a‖

The non negative norm seen as an ENNReal and then as a Real is equal to the norm.

theorem edist_eq_coe_nnnorm_div {E : Type u_5} [SeminormedGroup E] (a b : E) : edist a b = ↑‖a / b‖₊

theorem edist_eq_coe_nnnorm_sub {E : Type u_5} [SeminormedAddGroup E] (a b : E) : edist a b = ↑‖a - b‖₊

theorem edist_eq_coe_nnnorm' {E : Type u_5} [SeminormedGroup E] (x : E) : edist x 1 = ↑‖x‖₊

theorem edist_eq_coe_nnnorm {E : Type u_5} [SeminormedAddGroup E] (x : E) : edist x 0 = ↑‖x‖₊

theorem edist_mulIndicator {α : Type u_2} {E : Type u_5} [SeminormedGroup E] (s t : Set α) (f : α → E) (x : α) : edist (s.mulIndicator f x) (t.mulIndicator f x) = ↑‖(symmDiff s t).mulIndicator f x‖₊

theorem edist_indicator {α : Type u_2} {E : Type u_5} [SeminormedAddGroup E] (s t : Set α) (f : α → E) (x : α) : edist (s.indicator f x) (t.indicator f x) = ↑‖(symmDiff s t).indicator f x‖₊

theorem mem_emetric_ball_one_iff {E : Type u_5} [SeminormedGroup E] {a : E} {r : ENNReal} : a ∈ EMetric.ball 1 r ↔ ↑‖a‖₊ < r

theorem mem_emetric_ball_zero_iff {E : Type u_5} [SeminormedAddGroup E] {a : E} {r : ENNReal} : a ∈ EMetric.ball 0 r ↔ ↑‖a‖₊ < r

instance instENormOfNNNorm {E : Type u_8} [NNNorm E] : ENorm E

Equations

• instENormOfNNNorm = { enorm := fun (x : E) => ↑‖x‖₊ }

theorem enorm_eq_nnnorm {E : Type u_8} [NNNorm E] {x : E} : ‖x‖ₑ = ↑‖x‖₊

instance instENormENNReal : ENorm ENNReal

Equations

• instENormENNReal = { enorm := fun (x : ENNReal) => x }

@[simp]

theorem enorm_eq_self (x : ENNReal) : ‖x‖ₑ = x

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)

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)

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)

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)

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

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

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.

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.

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.

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.

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

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

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))

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))

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

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

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.

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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'

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'

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

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

@[reducible, inline]

abbrev SeminormedGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [Group E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedGroup E

A group homomorphism from a Group to a SeminormedGroup induces a SeminormedGroup structure on the domain.

Equations

• SeminormedGroup.induced E F f = SeminormedGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedAddGroup E

A group homomorphism from an AddGroup to a SeminormedAddGroup induces a SeminormedAddGroup structure on the domain.

Equations

• SeminormedAddGroup.induced E F f = SeminormedAddGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedCommGroup E

A group homomorphism from a CommGroup to a SeminormedGroup induces a SeminormedCommGroup structure on the domain.

Equations

• SeminormedCommGroup.induced E F f = SeminormedCommGroup.mk ⋯

@[reducible, inline]

abbrev SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddCommGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedAddCommGroup E

A group homomorphism from an AddCommGroup to a SeminormedAddGroup induces a SeminormedAddCommGroup structure on the domain.

Equations

• SeminormedAddCommGroup.induced E F f = SeminormedAddCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [Group E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedGroup E

An injective group homomorphism from a Group to a NormedGroup induces a NormedGroup structure on the domain.

Equations

• NormedGroup.induced E F f h = NormedGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedAddGroup E

An injective group homomorphism from an AddGroup to a NormedAddGroup induces a NormedAddGroup structure on the domain.

Equations

• NormedAddGroup.induced E F f h = NormedAddGroup.mk ⋯

@[reducible, inline]

abbrev NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedCommGroup E

An injective group homomorphism from a CommGroup to a NormedGroup induces a NormedCommGroup structure on the domain.

Equations

• NormedCommGroup.induced E F f h = NormedCommGroup.mk ⋯

@[reducible, inline]

abbrev NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [FunLike 𝓕 E F] [AddCommGroup E] [NormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (h : Function.Injective ⇑f) : NormedAddCommGroup E

An injective group homomorphism from a CommGroup to a NormedCommGroup induces a NormedCommGroup structure on the domain.

Equations

• NormedAddCommGroup.induced E F f h = NormedAddCommGroup.mk ⋯

theorem dist_inv {E : Type u_5} [SeminormedCommGroup E] (x y : E) : dist x⁻¹ y = dist x y⁻¹

theorem dist_neg {E : Type u_5} [SeminormedAddCommGroup E] (x y : E) : dist (-x) y = dist x (-y)

theorem norm_multiset_sum_le {E : Type u_8} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem norm_multiset_prod_le {E : Type u_5} [SeminormedCommGroup E] (m : Multiset E) : ‖m.prod‖ ≤ (Multiset.map (fun (x : E) => ‖x‖) m).sum

theorem norm_sum_le {ι : Type u_8} {E : Type u_9} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

theorem norm_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖∏ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

theorem norm_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖∏ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b

theorem norm_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖∑ b ∈ s, f b‖ ≤ ∑ b ∈ s, n b

theorem dist_prod_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

theorem dist_sum_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, d b

theorem dist_prod_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f a : ι → E) : dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

theorem dist_sum_sum_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) (f a : ι → E) : dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b)

theorem mul_mem_ball_iff_norm {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem add_mem_ball_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.ball a r ↔ ‖b‖ < r

theorem mul_mem_closedBall_iff_norm {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a * b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

theorem add_mem_closedBall_iff_norm {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r

@[simp]

theorem preimage_mul_ball {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r

@[simp]

theorem preimage_add_ball {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.ball a r = Metric.ball (a - b) r

@[simp]

theorem preimage_mul_closedBall {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a / b) r

@[simp]

theorem preimage_add_closedBall {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.closedBall a r = Metric.closedBall (a - b) r

@[simp]

theorem preimage_mul_sphere {E : Type u_5} [SeminormedCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b * x) ⁻¹' Metric.sphere a r = Metric.sphere (a / b) r

@[simp]

theorem preimage_add_sphere {E : Type u_5} [SeminormedAddCommGroup E] (a b : E) (r : ℝ) : (fun (x : E) => b + x) ⁻¹' Metric.sphere a r = Metric.sphere (a - b) r

theorem pow_mem_closedBall {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : a ^ n ∈ Metric.closedBall (b ^ n) (n • r)

theorem nsmul_mem_closedBall {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (h : a ∈ Metric.closedBall b r) : n • a ∈ Metric.closedBall (n • b) (n • r)

theorem pow_mem_ball {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : a ^ n ∈ Metric.ball (b ^ n) (n • r)

theorem nsmul_mem_ball {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {n : ℕ} (hn : 0 < n) (h : a ∈ Metric.ball b r) : n • a ∈ Metric.ball (n • b) (n • r)

theorem mul_mem_closedBall_mul_iff {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.closedBall (b * c) r ↔ a ∈ Metric.closedBall b r

theorem add_mem_closedBall_add_iff {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.closedBall (b + c) r ↔ a ∈ Metric.closedBall b r

theorem mul_mem_ball_mul_iff {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} {c : E} : a * c ∈ Metric.ball (b * c) r ↔ a ∈ Metric.ball b r

theorem add_mem_ball_add_iff {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E} : a + c ∈ Metric.ball (b + c) r ↔ a ∈ Metric.ball b r

theorem smul_closedBall'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.closedBall b r = Metric.closedBall (a • b) r

theorem vadd_closedBall'' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.closedBall b r = Metric.closedBall (a +ᵥ b) r

theorem smul_ball'' {E : Type u_5} [SeminormedCommGroup E] {a b : E} {r : ℝ} : a • Metric.ball b r = Metric.ball (a • b) r

theorem vadd_ball'' {E : Type u_5} [SeminormedAddCommGroup E] {a b : E} {r : ℝ} : a +ᵥ Metric.ball b r = Metric.ball (a +ᵥ b) r

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

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

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

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

theorem nnnorm_multiset_prod_le {E : Type u_5} [SeminormedCommGroup E] (m : Multiset E) : ‖m.prod‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

theorem nnnorm_multiset_sum_le {E : Type u_5} [SeminormedAddCommGroup E] (m : Multiset E) : ‖m.sum‖₊ ≤ (Multiset.map (fun (x : E) => ‖x‖₊) m).sum

theorem nnnorm_prod_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

theorem nnnorm_sum_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊

theorem nnnorm_prod_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖∏ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

theorem nnnorm_sum_le_of_le {ι : Type u_3} {E : Type u_5} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖∑ b ∈ s, f b‖₊ ≤ ∑ b ∈ s, n b

instance Real.norm : Norm ℝ

Equations

• Real.norm = { norm := fun (r : ℝ) => |r| }

@[simp]

theorem Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|

instance Real.normedAddCommGroup : NormedAddCommGroup ℝ

Equations

• Real.normedAddCommGroup = NormedAddCommGroup.mk Real.normedAddCommGroup.proof_1

theorem Real.norm_of_nonneg {r : ℝ} (hr : 0 ≤ r) : ‖r‖ = r

theorem Real.norm_of_nonpos {r : ℝ} (hr : r ≤ 0) : ‖r‖ = -r

theorem Real.le_norm_self (r : ℝ) : r ≤ ‖r‖

@[simp]

theorem Real.norm_natCast (n : ℕ) : ‖↑n‖ = ↑n

@[simp]

theorem Real.nnnorm_natCast (n : ℕ) : ‖↑n‖₊ = ↑n

@[deprecated Real.norm_natCast (since := "2024-04-05")]

theorem Real.norm_coe_nat (n : ℕ) : ‖↑n‖ = ↑n

Alias of Real.norm_natCast.

@[deprecated Real.nnnorm_natCast (since := "2024-04-05")]

theorem Real.nnnorm_coe_nat (n : ℕ) : ‖↑n‖₊ = ↑n

Alias of Real.nnnorm_natCast.

@[simp]

theorem Real.norm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖ = OfNat.ofNat n

@[simp]

theorem Real.nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖₊ = OfNat.ofNat n

theorem Real.norm_two : ‖2‖ = 2

theorem Real.nnnorm_two : ‖2‖₊ = 2

@[simp]

theorem Real.norm_nnratCast (q : ℚ≥0) : ‖↑q‖ = ↑q

@[simp]

theorem Real.nnnorm_nnratCast (q : ℚ≥0) : ‖↑q‖₊ = ↑q

theorem Real.nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) : ‖r‖₊ = ⟨r, hr⟩

@[simp]

theorem Real.nnnorm_abs (r : ℝ) : ‖|r|‖₊ = ‖r‖₊

theorem Real.ennnorm_eq_ofReal {r : ℝ} (hr : 0 ≤ r) : ↑‖r‖₊ = ENNReal.ofReal r

theorem Real.ennnorm_eq_ofReal_abs (r : ℝ) : ↑‖r‖₊ = ENNReal.ofReal |r|

theorem Real.toNNReal_eq_nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) : r.toNNReal = ‖r‖₊

theorem Real.ofReal_le_ennnorm (r : ℝ) : ENNReal.ofReal r ≤ ↑‖r‖₊

instance NNReal.instNNNorm : NNNorm NNReal

Equations

• NNReal.instNNNorm = { nnnorm := fun (x : NNReal) => x }

@[simp]

theorem NNReal.nnnorm_eq_self (x : NNReal) : ‖x‖₊ = x

@[simp]

theorem norm_le_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1

@[simp]

theorem norm_le_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 0

@[simp]

theorem norm_pos_iff' {E : Type u_5} [NormedGroup E] {a : E} : 0 < ‖a‖ ↔ a ≠ 1

@[simp]

theorem norm_pos_iff {E : Type u_5} [NormedAddGroup E] {a : E} : 0 < ‖a‖ ↔ a ≠ 0

@[simp]

theorem norm_eq_zero' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ = 0 ↔ a = 1

@[simp]

theorem norm_eq_zero {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ = 0 ↔ a = 0

theorem norm_ne_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≠ 0 ↔ a ≠ 1

theorem norm_ne_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖ ≠ 0 ↔ a ≠ 0

@[deprecated norm_le_zero_iff' (since := "2024-11-24")]

theorem norm_le_zero_iff'' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1

Alias of norm_le_zero_iff'.

@[deprecated norm_le_zero_iff' (since := "2024-11-24")]

theorem norm_le_zero_iff''' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1

Alias of norm_le_zero_iff'.

@[deprecated norm_pos_iff' (since := "2024-11-24")]

theorem norm_pos_iff'' {E : Type u_5} [NormedGroup E] {a : E} : 0 < ‖a‖ ↔ a ≠ 1

Alias of norm_pos_iff'.

@[deprecated norm_eq_zero' (since := "2024-11-24")]

theorem norm_eq_zero'' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ = 0 ↔ a = 1

Alias of norm_eq_zero'.

@[deprecated norm_eq_zero' (since := "2024-11-24")]

theorem norm_eq_zero''' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖ = 0 ↔ a = 1

Alias of norm_eq_zero'.

theorem norm_div_eq_zero_iff {E : Type u_5} [NormedGroup E] {a b : E} : ‖a / b‖ = 0 ↔ a = b

theorem norm_sub_eq_zero_iff {E : Type u_5} [NormedAddGroup E] {a b : E} : ‖a - b‖ = 0 ↔ a = b

theorem norm_div_pos_iff {E : Type u_5} [NormedGroup E] {a b : E} : 0 < ‖a / b‖ ↔ a ≠ b

theorem norm_sub_pos_iff {E : Type u_5} [NormedAddGroup E] {a b : E} : 0 < ‖a - b‖ ↔ a ≠ b

theorem eq_of_norm_div_le_zero {E : Type u_5} [NormedGroup E] {a b : E} (h : ‖a / b‖ ≤ 0) : a = b

theorem eq_of_norm_sub_le_zero {E : Type u_5} [NormedAddGroup E] {a b : E} (h : ‖a - b‖ ≤ 0) : a = b

theorem eq_of_norm_div_eq_zero {E : Type u_5} [NormedGroup E] {a b : E} : ‖a / b‖ = 0 → a = b

Alias of the forward direction of norm_div_eq_zero_iff.

theorem eq_of_norm_sub_eq_zero {E : Type u_5} [NormedAddGroup E] {a b : E} : ‖a - b‖ = 0 → a = b

theorem eq_one_or_norm_pos {E : Type u_5} [NormedGroup E] (a : E) : a = 1 ∨ 0 < ‖a‖

theorem eq_zero_or_norm_pos {E : Type u_5} [NormedAddGroup E] (a : E) : a = 0 ∨ 0 < ‖a‖

theorem eq_one_or_nnnorm_pos {E : Type u_5} [NormedGroup E] (a : E) : a = 1 ∨ 0 < ‖a‖₊

theorem eq_zero_or_nnnorm_pos {E : Type u_5} [NormedAddGroup E] (a : E) : a = 0 ∨ 0 < ‖a‖₊

@[simp]

theorem nnnorm_eq_zero' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖₊ = 0 ↔ a = 1

@[simp]

theorem nnnorm_eq_zero {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖₊ = 0 ↔ a = 0

theorem nnnorm_ne_zero_iff' {E : Type u_5} [NormedGroup E] {a : E} : ‖a‖₊ ≠ 0 ↔ a ≠ 1

theorem nnnorm_ne_zero_iff {E : Type u_5} [NormedAddGroup E] {a : E} : ‖a‖₊ ≠ 0 ↔ a ≠ 0

@[simp]

theorem nnnorm_pos' {E : Type u_5} [NormedGroup E] {a : E} : 0 < ‖a‖₊ ↔ a ≠ 1

@[simp]

theorem nnnorm_pos {E : Type u_5} [NormedAddGroup E] {a : E} : 0 < ‖a‖₊ ↔ a ≠ 0

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.

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.

@[deprecated tendsto_norm_nhdsNE_zero (since := "2024-12-22")]

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

Alias of tendsto_norm_nhdsNE_zero.

---

See tendsto_norm_zero for a version with full neighborhoods.

@[deprecated tendsto_norm_nhdsNE_one (since := "2024-12-22")]

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

Alias of tendsto_norm_nhdsNE_one.

---

See tendsto_norm_one for a version with full neighborhoods.

@[deprecated tendsto_norm_nhdsNE_zero (since := "2024-12-22")]

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

Alias of tendsto_norm_nhdsNE_zero.

---

See tendsto_norm_zero for a version with full neighborhoods.

@[deprecated tendsto_norm_nhdsNE_one (since := "2024-12-22")]

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

Alias of tendsto_norm_nhdsNE_one.

---

See tendsto_norm_one for a version with full neighborhoods.

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))

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))

@[deprecated tendsto_norm_sub_self_nhdsNE (since := "2024-12-22")]

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

Alias of tendsto_norm_sub_self_nhdsNE.

@[deprecated tendsto_norm_div_self_nhdsNE (since := "2024-12-22")]

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

Alias of tendsto_norm_div_self_nhdsNE.

def normGroupNorm (E : Type u_5) [NormedGroup E] : GroupNorm E

The norm of a normed group as a group norm.

Equations

• normGroupNorm E = { toGroupSeminorm := normGroupSeminorm E, eq_one_of_map_eq_zero' := ⋯ }

def normAddGroupNorm (E : Type u_5) [NormedAddGroup E] : AddGroupNorm E

The norm of a normed group as an additive group norm.

Equations

• normAddGroupNorm E = { toAddGroupSeminorm := normAddGroupSeminorm E, eq_zero_of_map_eq_zero' := ⋯ }

@[simp]

theorem coe_normGroupNorm (E : Type u_5) [NormedGroup E] : ⇑(normGroupNorm E) = norm

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.

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

@[deprecated comap_norm_nhdsGT_zero (since := "2024-12-22")]

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

Alias of comap_norm_nhdsGT_zero.

@[deprecated comap_norm_nhdsGT_zero' (since := "2024-12-22")]

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

Alias of comap_norm_nhdsGT_zero'.

---

A version of comap_norm_nhdsGT_zero for a multiplicative normed group.

Some relations with HasCompactSupport

theorem hasCompactSupport_norm_iff {α : Type u_2} {E : Type u_5} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : (HasCompactSupport fun (x : α) => ‖f x‖) ↔ HasCompactSupport f

theorem HasCompactSupport.norm {α : Type u_2} {E : Type u_5} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} : HasCompactSupport f → HasCompactSupport fun (x : α) => ‖f x‖

Alias of the reverse direction of hasCompactSupport_norm_iff.

positivity extensions

def Mathlib.Meta.Positivity.evalMulNorm : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: multiplicative norms are always nonnegative, and positive on non-one inputs.

def Mathlib.Meta.Positivity.evalAddNorm : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: additive norms are always nonnegative, and positive on non-zero inputs.

Subgroups of normed groups

instance Subgroup.seminormedGroup {E : Type u_5} [SeminormedGroup E] {s : Subgroup E} : SeminormedGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

• Subgroup.seminormedGroup = SeminormedGroup.induced (↥s) E s.subtype

instance AddSubgroup.seminormedAddGroup {E : Type u_5} [SeminormedAddGroup E] {s : AddSubgroup E} : SeminormedAddGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

• AddSubgroup.seminormedAddGroup = SeminormedAddGroup.induced (↥s) E s.subtype

@[simp]

theorem Subgroup.coe_norm {E : Type u_5} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

@[simp]

theorem AddSubgroup.coe_norm {E : Type u_5} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

theorem Subgroup.norm_coe {E : Type u_5} [SeminormedGroup E] {s : Subgroup E} (x : ↥s) : ‖↑x‖ = ‖x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma Subgroup.coe_norm for use by norm_cast.

theorem AddSubgroup.norm_coe {E : Type u_5} [SeminormedAddGroup E] {s : AddSubgroup E} (x : ↥s) : ‖↑x‖ = ‖x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

This is a reversed version of the simp lemma AddSubgroup.coe_norm for use by norm_cast.

instance Subgroup.seminormedCommGroup {E : Type u_5} [SeminormedCommGroup E] {s : Subgroup E} : SeminormedCommGroup ↥s

Equations

• Subgroup.seminormedCommGroup = SeminormedCommGroup.induced (↥s) E s.subtype

instance AddSubgroup.seminormedAddCommGroup {E : Type u_5} [SeminormedAddCommGroup E] {s : AddSubgroup E} : SeminormedAddCommGroup ↥s

Equations

• AddSubgroup.seminormedAddCommGroup = SeminormedAddCommGroup.induced (↥s) E s.subtype

instance Subgroup.normedGroup {E : Type u_5} [NormedGroup E] {s : Subgroup E} : NormedGroup ↥s

Equations

• Subgroup.normedGroup = NormedGroup.induced (↥s) E s.subtype ⋯

instance AddSubgroup.normedAddGroup {E : Type u_5} [NormedAddGroup E] {s : AddSubgroup E} : NormedAddGroup ↥s

Equations

• AddSubgroup.normedAddGroup = NormedAddGroup.induced (↥s) E s.subtype ⋯

instance Subgroup.normedCommGroup {E : Type u_5} [NormedCommGroup E] {s : Subgroup E} : NormedCommGroup ↥s

Equations

• Subgroup.normedCommGroup = NormedCommGroup.induced (↥s) E s.subtype ⋯

instance AddSubgroup.normedAddCommGroup {E : Type u_5} [NormedAddCommGroup E] {s : AddSubgroup E} : NormedAddCommGroup ↥s

Equations

• AddSubgroup.normedAddCommGroup = NormedAddCommGroup.induced (↥s) E s.subtype ⋯

Subgroup classes of normed groups

@[instance 75]

instance SubgroupClass.seminormedGroup {E : Type u_5} [SeminormedGroup E] {S : Type u_8} [SetLike S E] [SubgroupClass S E] (s : S) : SeminormedGroup ↥s

A subgroup of a seminormed group is also a seminormed group, with the restriction of the norm.

Equations

• SubgroupClass.seminormedGroup s = SeminormedGroup.induced (↥s) E ↑s

@[instance 75]

instance AddSubgroupClass.seminormedAddGroup {E : Type u_5} [SeminormedAddGroup E] {S : Type u_8} [SetLike S E] [AddSubgroupClass S E] (s : S) : SeminormedAddGroup ↥s

A subgroup of a seminormed additive group is also a seminormed additive group, with the restriction of the norm.

Equations

• AddSubgroupClass.seminormedAddGroup s = SeminormedAddGroup.induced (↥s) E ↑s

@[simp]

theorem SubgroupClass.coe_norm {E : Type u_5} [SeminormedGroup E] {S : Type u_8} [SetLike S E] [SubgroupClass S E] (s : S) (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of a subgroup s of a seminormed group E, its norm in s is equal to its norm in E.

@[simp]

theorem AddSubgroupClass.coe_norm {E : Type u_5} [SeminormedAddGroup E] {S : Type u_8} [SetLike S E] [AddSubgroupClass S E] (s : S) (x : ↥s) : ‖x‖ = ‖↑x‖

If x is an element of an additive subgroup s of a seminormed additive group E, its norm in s is equal to its norm in E.

@[instance 75]

instance SubgroupClass.seminormedCommGroup {E : Type u_5} [SeminormedCommGroup E] {S : Type u_8} [SetLike S E] [SubgroupClass S E] (s : S) : SeminormedCommGroup ↥s

Equations

• SubgroupClass.seminormedCommGroup s = SeminormedCommGroup.induced (↥s) E ↑s

@[instance 75]

instance AddSubgroupClass.seminormedAddCommGroup {E : Type u_5} [SeminormedAddCommGroup E] {S : Type u_8} [SetLike S E] [AddSubgroupClass S E] (s : S) : SeminormedAddCommGroup ↥s

Equations

• AddSubgroupClass.seminormedAddCommGroup s = SeminormedAddCommGroup.induced (↥s) E ↑s

@[instance 75]

instance SubgroupClass.normedGroup {E : Type u_5} [NormedGroup E] {S : Type u_8} [SetLike S E] [SubgroupClass S E] (s : S) : NormedGroup ↥s

Equations

• SubgroupClass.normedGroup s = NormedGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance AddSubgroupClass.normedAddGroup {E : Type u_5} [NormedAddGroup E] {S : Type u_8} [SetLike S E] [AddSubgroupClass S E] (s : S) : NormedAddGroup ↥s

Equations

• AddSubgroupClass.normedAddGroup s = NormedAddGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance SubgroupClass.normedCommGroup {E : Type u_5} [NormedCommGroup E] {S : Type u_8} [SetLike S E] [SubgroupClass S E] (s : S) : NormedCommGroup ↥s

Equations

• SubgroupClass.normedCommGroup s = NormedCommGroup.induced (↥s) E ↑s ⋯

@[instance 75]

instance AddSubgroupClass.normedAddCommGroup {E : Type u_5} [NormedAddCommGroup E] {S : Type u_8} [SetLike S E] [AddSubgroupClass S E] (s : S) : NormedAddCommGroup ↥s

Equations

• AddSubgroupClass.normedAddCommGroup s = NormedAddCommGroup.induced (↥s) E ↑s ⋯

theorem tendsto_norm_atTop_atTop : Filter.Tendsto norm Filter.atTop Filter.atTop