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_9) : Type u_9

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_9) : Type u_9

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

• nnnorm : E → NNReal

  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.

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

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 (Int.ofNat (Nat.succ n)) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_9) extends Norm , Group , PseudoMetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = DivInvMonoid.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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_9) extends Norm , AddGroup , MetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_9) extends Norm , Group , MetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = DivInvMonoid.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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_9) extends Norm , AddCommGroup , PseudoMetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_9) extends Norm , CommGroup , PseudoMetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = DivInvMonoid.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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_9) extends Norm , AddCommGroup , MetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = SubNegMonoid.zsmul (Int.ofNat n) a + a
• zsmul_neg' : ∀ (n : ℕ) (a : E), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_9) extends Norm , CommGroup , MetricSpace : Type u_9

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 (Int.ofNat (Nat.succ n)) a = DivInvMonoid.zpow (Int.ofNat n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : E), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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 NormedAddGroup.toSeminormedAddGroup {E : Type u_6} [NormedAddGroup E] : SeminormedAddGroup E

Equations

• NormedAddGroup.toSeminormedAddGroup = let __src := inst; SeminormedAddGroup.mk ⋯

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

Equations

• NormedGroup.toSeminormedGroup = let __src := inst; SeminormedGroup.mk ⋯

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

Equations

• NormedAddCommGroup.toSeminormedAddCommGroup = let __src := inst; SeminormedAddCommGroup.mk ⋯

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

Equations

• NormedCommGroup.toSeminormedCommGroup = let __src := inst; SeminormedCommGroup.mk ⋯

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

Equations

• SeminormedAddCommGroup.toSeminormedAddGroup = let __src := inst; SeminormedAddGroup.mk ⋯

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

Equations

• SeminormedCommGroup.toSeminormedGroup = let __src := inst; SeminormedGroup.mk ⋯

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

Equations

• NormedAddCommGroup.toNormedAddGroup = let __src := inst; NormedAddGroup.mk ⋯

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

Equations

• NormedCommGroup.toNormedGroup = let __src := inst; NormedGroup.mk ⋯

@[reducible]

def NormedAddGroup.ofSeparation {E : Type u_6} [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 ⋯

theorem NormedAddGroup.ofSeparation.proof_1 {E : Type u_1} [SeminormedAddGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) : ∀ {x y : E}, dist x y = 0 → x = y

@[reducible]

def NormedGroup.ofSeparation {E : Type u_6} [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 ⋯

theorem NormedAddCommGroup.ofSeparation.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] (h : ∀ (x : E), ‖x‖ = 0 → x = 0) : ∀ {x y : E}, dist x y = 0 → x = y

@[reducible]

def NormedAddCommGroup.ofSeparation {E : Type u_6} [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 = let __src := inst; let __src_1 := NormedAddGroup.ofSeparation h; NormedAddCommGroup.mk ⋯

@[reducible]

def NormedCommGroup.ofSeparation {E : Type u_6} [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 = let __src := inst; let __src_1 := NormedGroup.ofSeparation h; NormedCommGroup.mk ⋯

theorem SeminormedAddGroup.ofAddDist.proof_1 {E : Type u_1} [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)) (x : E) (y : E) : dist x y = ‖x - y‖

@[reducible]

def SeminormedAddGroup.ofAddDist {E : Type u_6} [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]

def SeminormedGroup.ofMulDist {E : Type u_6} [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]

def SeminormedAddGroup.ofAddDist' {E : Type u_6} [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 ⋯

theorem SeminormedAddGroup.ofAddDist'.proof_1 {E : Type u_1} [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) (x : E) (y : E) : dist x y = ‖x - y‖

@[reducible]

def SeminormedGroup.ofMulDist' {E : Type u_6} [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]

def SeminormedAddCommGroup.ofAddDist {E : Type u_6} [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₂ = let __src := SeminormedAddGroup.ofAddDist h₁ h₂; SeminormedAddCommGroup.mk ⋯

theorem SeminormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def SeminormedCommGroup.ofMulDist {E : Type u_6} [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₂ = let __src := SeminormedGroup.ofMulDist h₁ h₂; SeminormedCommGroup.mk ⋯

@[reducible]

def SeminormedAddCommGroup.ofAddDist' {E : Type u_6} [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₂ = let __src := SeminormedAddGroup.ofAddDist' h₁ h₂; SeminormedAddCommGroup.mk ⋯

theorem SeminormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def SeminormedCommGroup.ofMulDist' {E : Type u_6} [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₂ = let __src := SeminormedGroup.ofMulDist' h₁ h₂; SeminormedCommGroup.mk ⋯

@[reducible]

def NormedAddGroup.ofAddDist {E : Type u_6} [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₂ = let __src := SeminormedAddGroup.ofAddDist h₁ h₂; NormedAddGroup.mk ⋯

@[reducible]

def NormedGroup.ofMulDist {E : Type u_6} [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₂ = let __src := SeminormedGroup.ofMulDist h₁ h₂; NormedGroup.mk ⋯

@[reducible]

def NormedAddGroup.ofAddDist' {E : Type u_6} [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₂ = let __src := SeminormedAddGroup.ofAddDist' h₁ h₂; NormedAddGroup.mk ⋯

@[reducible]

def NormedGroup.ofMulDist' {E : Type u_6} [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₂ = let __src := SeminormedGroup.ofMulDist' h₁ h₂; NormedGroup.mk ⋯

theorem NormedAddCommGroup.ofAddDist.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def NormedAddCommGroup.ofAddDist {E : Type u_6} [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₂ = let __src := NormedAddGroup.ofAddDist h₁ h₂; NormedAddCommGroup.mk ⋯

@[reducible]

def NormedCommGroup.ofMulDist {E : Type u_6} [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₂ = let __src := NormedGroup.ofMulDist h₁ h₂; NormedCommGroup.mk ⋯

@[reducible]

def NormedAddCommGroup.ofAddDist' {E : Type u_6} [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₂ = let __src := NormedAddGroup.ofAddDist' h₁ h₂; NormedAddCommGroup.mk ⋯

theorem NormedAddCommGroup.ofAddDist'.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def NormedCommGroup.ofMulDist' {E : Type u_6} [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₂ = let __src := NormedGroup.ofMulDist' h₁ h₂; NormedCommGroup.mk ⋯

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) : f (x - x) = 0

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_2 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) : f (x - y) = f (y - x)

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_3 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (a : E) (b : E) (c : E) : f (a - c) ≤ f (a - b) + f (b - c)

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_4 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) : 0 ≤ f (x - y)

@[reducible]

def AddGroupSeminorm.toSeminormedAddGroup {E : Type u_6} [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

• AddGroupSeminorm.toSeminormedAddGroup f = SeminormedAddGroup.mk ⋯

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_7 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) : (Bornology.cobounded E).sets = (Bornology.cobounded E).sets

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_8 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) : dist x y = dist x y

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_5 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) (x : E) (y : E) : ↑{ val := f (x - y), property := ⋯ } = ENNReal.ofReal ↑{ val := f (x - y), property := ⋯ }

theorem AddGroupSeminorm.toSeminormedAddGroup.proof_6 {E : Type u_1} [AddGroup E] (f : AddGroupSeminorm E) : uniformity E = uniformity E

@[reducible]

def GroupSeminorm.toSeminormedGroup {E : Type u_6} [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

• GroupSeminorm.toSeminormedGroup f = SeminormedGroup.mk ⋯

theorem AddGroupSeminorm.toSeminormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def AddGroupSeminorm.toSeminormedAddCommGroup {E : Type u_6} [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

• AddGroupSeminorm.toSeminormedAddCommGroup f = let __src := AddGroupSeminorm.toSeminormedAddGroup f; SeminormedAddCommGroup.mk ⋯

@[reducible]

def GroupSeminorm.toSeminormedCommGroup {E : Type u_6} [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

• GroupSeminorm.toSeminormedCommGroup f = let __src := GroupSeminorm.toSeminormedGroup f; SeminormedCommGroup.mk ⋯

@[reducible]

def AddGroupNorm.toNormedAddGroup {E : Type u_6} [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

• AddGroupNorm.toNormedAddGroup f = let __src := AddGroupSeminorm.toSeminormedAddGroup f.toAddGroupSeminorm; NormedAddGroup.mk ⋯

theorem AddGroupNorm.toNormedAddGroup.proof_1 {E : Type u_1} [AddGroup E] (f : AddGroupNorm E) : ∀ {x y : E}, dist x y = 0 → x = y

@[reducible]

def GroupNorm.toNormedGroup {E : Type u_6} [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

• GroupNorm.toNormedGroup f = let __src := GroupSeminorm.toSeminormedGroup f.toGroupSeminorm; NormedGroup.mk ⋯

@[reducible]

def AddGroupNorm.toNormedAddCommGroup {E : Type u_6} [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

• AddGroupNorm.toNormedAddCommGroup f = let __src := AddGroupNorm.toNormedAddGroup f; NormedAddCommGroup.mk ⋯

theorem AddGroupNorm.toNormedAddCommGroup.proof_1 {E : Type u_1} [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def GroupNorm.toNormedCommGroup {E : Type u_6} [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

• GroupNorm.toNormedCommGroup f = let __src := GroupNorm.toNormedGroup f; NormedCommGroup.mk ⋯

instance PUnit.normedAddCommGroup : NormedAddCommGroup PUnit.{u_9 + 1}

Equations

• PUnit.normedAddCommGroup = NormedAddCommGroup.mk PUnit.normedAddCommGroup.proof_1

@[simp]

theorem PUnit.norm_eq_zero (r : PUnit.{u_9 + 1} ) : ‖r‖ = 0

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

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

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

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

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

Alias of dist_eq_norm_sub.

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

Alias of dist_eq_norm_sub'.

instance NormedAddGroup.to_isometricVAdd_right {E : Type u_6} [SeminormedAddGroup E] : IsometricVAdd Eᵃᵒᵖ E

Equations

• ⋯ = ⋯

instance NormedGroup.to_isometricSMul_right {E : Type u_6} [SeminormedGroup E] : IsometricSMul Eᵐᵒᵖ E

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Isometry.norm_map_of_map_zero {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) : ‖f x‖ = ‖x‖

theorem Isometry.norm_map_of_map_one {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖ = ‖x‖

@[simp]

theorem comap_norm_atTop {E : Type u_6} [SeminormedAddGroup E] : Filter.comap norm Filter.atTop = Bornology.cobounded E

@[simp]

theorem comap_norm_atTop' {E : Type u_6} [SeminormedGroup E] : Filter.comap norm Filter.atTop = Bornology.cobounded E

theorem Filter.HasBasis.cobounded_of_norm {E : Type u_6} [SeminormedAddGroup E] {ι : Sort u_9} {p : ι → Prop} {s : ι → Set ℝ} (h : Filter.HasBasis Filter.atTop p s) : Filter.HasBasis (Bornology.cobounded E) p fun (i : ι) => norm ⁻¹' s i

theorem Filter.HasBasis.cobounded_of_norm' {E : Type u_6} [SeminormedGroup E] {ι : Sort u_9} {p : ι → Prop} {s : ι → Set ℝ} (h : Filter.HasBasis Filter.atTop p s) : Filter.HasBasis (Bornology.cobounded E) p fun (i : ι) => norm ⁻¹' s i

theorem Filter.hasBasis_cobounded_norm {E : Type u_6} [SeminormedAddGroup E] : Filter.HasBasis (Bornology.cobounded E) (fun (x : ℝ) => True) fun (x : ℝ) => {x_1 : E | x ≤ ‖x_1‖}

theorem Filter.hasBasis_cobounded_norm' {E : Type u_6} [SeminormedGroup E] : Filter.HasBasis (Bornology.cobounded E) (fun (x : ℝ) => True) fun (x : ℝ) => {x_1 : E | x ≤ ‖x_1‖}

@[simp]

theorem tendsto_norm_atTop_iff_cobounded {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto (fun (x : α) => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)

@[simp]

theorem tendsto_norm_atTop_iff_cobounded' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] {f : α → E} {l : Filter α} : Filter.Tendsto (fun (x : α) => ‖f x‖) l Filter.atTop ↔ Filter.Tendsto f l (Bornology.cobounded E)

theorem tendsto_norm_cobounded_atTop {E : Type u_6} [SeminormedAddGroup E] : Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop

theorem tendsto_norm_cobounded_atTop' {E : Type u_6} [SeminormedGroup E] : Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop

theorem eventually_cobounded_le_norm {E : Type u_6} [SeminormedAddGroup E] (a : ℝ) : ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖

theorem eventually_cobounded_le_norm' {E : Type u_6} [SeminormedGroup E] (a : ℝ) : ∀ᶠ (x : E) in Bornology.cobounded E, a ≤ ‖x‖

theorem tendsto_norm_cocompact_atTop {E : Type u_6} [SeminormedAddGroup E] [ProperSpace E] : Filter.Tendsto norm (Filter.cocompact E) Filter.atTop

theorem tendsto_norm_cocompact_atTop' {E : Type u_6} [SeminormedGroup E] [ProperSpace E] : Filter.Tendsto norm (Filter.cocompact E) Filter.atTop

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem dist_add_self_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) : dist b (a + b) = ‖a‖

@[simp]

theorem dist_mul_self_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) : dist b (a * b) = ‖a‖

@[simp]

theorem dist_add_self_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) : dist (a + b) b = ‖a‖

@[simp]

theorem dist_mul_self_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) : dist (a * b) b = ‖a‖

@[simp]

theorem dist_sub_eq_dist_add_left {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) : dist (a - b) c = dist a (c + b)

@[simp]

theorem dist_div_eq_dist_mul_left {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) : dist (a / b) c = dist a (c * b)

@[simp]

theorem dist_sub_eq_dist_add_right {E : Type u_6} [SeminormedAddGroup E] (a : E) (b : E) (c : E) : dist a (b - c) = dist (a + c) b

@[simp]

theorem dist_div_eq_dist_mul_right {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) : dist a (b / c) = dist (a * c) b

@[simp]

theorem Filter.neg_cobounded {E : Type u_6} [SeminormedAddGroup E] : -Bornology.cobounded E = Bornology.cobounded E

@[simp]

theorem Filter.inv_cobounded {E : Type u_6} [SeminormedGroup E] : (Bornology.cobounded E)⁻¹ = Bornology.cobounded E

theorem Filter.tendsto_neg_cobounded {E : Type u_6} [SeminormedAddGroup E] : Filter.Tendsto Neg.neg (Bornology.cobounded E) (Bornology.cobounded E)

In a (semi)normed group, negation x ↦ -x tends to infinity at infinity.

theorem Filter.tendsto_inv_cobounded {E : Type u_6} [SeminormedGroup E] : Filter.Tendsto Inv.inv (Bornology.cobounded E) (Bornology.cobounded E)

In a (semi)normed group, inversion x ↦ x⁻¹ tends to infinity at infinity.

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

Triangle inequality for the norm.

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

Triangle inequality for the norm.

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

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

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

theorem norm_mul₃_le {E : Type u_6} [SeminormedGroup E] (a : E) (b : E) (c : E) : ‖a * b * c‖ ≤ ‖a‖ + ‖b‖ + ‖c‖

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Extension for the positivity tactic: multiplicative norms are nonnegative, via norm_nonneg'.

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

Extension for the positivity tactic: additive norms are nonnegative, via norm_nonneg.

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Alias of norm_le_norm_add_norm_sub'.

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

Alias of norm_le_norm_add_norm_sub.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem isBounded_iff_forall_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} : Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

theorem isBounded_iff_forall_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} : Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

theorem Bornology.IsBounded.exists_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} : Bornology.IsBounded s → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Alias of the forward direction of isBounded_iff_forall_norm_le'.

theorem Bornology.IsBounded.exists_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} : Bornology.IsBounded s → ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C

Alias of the forward direction of isBounded_iff_forall_norm_le.

theorem Bornology.IsBounded.exists_pos_norm_le {E : Type u_6} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

abbrev Bornology.IsBounded.exists_pos_norm_le.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C) → Prop) : ∀ (x : ∃ (C : ℝ), ∀ x ∈ s, ‖x‖ ≤ C), (∀ (R₀ : ℝ) (hR₀ : ∀ x ∈ s, ‖x‖ ≤ R₀), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Bornology.IsBounded.exists_pos_norm_le' {E : Type u_6} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R

abbrev Bornology.IsBounded.exists_pos_norm_lt.match_1 {E : Type u_1} [SeminormedAddGroup E] {s : Set E} (motive : (∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R) → Prop) : ∀ (x : ∃ R > 0, ∀ x ∈ s, ‖x‖ ≤ R), (∀ (R : ℝ) (hR₀ : R > 0) (hR : ∀ x ∈ s, ‖x‖ ≤ R), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Bornology.IsBounded.exists_pos_norm_lt {E : Type u_6} [SeminormedAddGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R

theorem Bornology.IsBounded.exists_pos_norm_lt' {E : Type u_6} [SeminormedGroup E] {s : Set E} (hs : Bornology.IsBounded s) : ∃ R > 0, ∀ x ∈ s, ‖x‖ < R

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

def normAddGroupSeminorm (E : Type u_6) [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' := ⋯ }

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

The norm of a seminormed group as a group seminorm.

Equations

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

@[simp]

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

@[simp]

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

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

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

theorem NormedAddCommGroup.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [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.tendsto_nhds_nhds {E : Type u_6} {F : Type u_7} [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.cauchySeq_iff {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [Nonempty α] [SemilatticeSup α] {u : α → E} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m - u n‖ < ε

theorem NormedCommGroup.cauchySeq_iff {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [Nonempty α] [SemilatticeSup α] {u : α → E} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : α), ∀ (m : α), N ≤ m → ∀ (n : α), N ≤ n → ‖u m / u n‖ < ε

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

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

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

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

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

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

theorem AddMonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : LipschitzWith (Real.toNNReal C) ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

theorem MonoidHomClass.lipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : LipschitzWith (Real.toNNReal C) ⇑f

A homomorphism f of seminormed groups is Lipschitz, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖. The analogous condition for a linear map of (semi)normed spaces is in Mathlib/Analysis/NormedSpace/OperatorNorm.lean.

theorem lipschitzOnWith_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem lipschitzOnWith_iff_norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

theorem LipschitzOnWith.norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitzOnWith_iff_norm_div_le.

theorem LipschitzOnWith.norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {f : E → F} {C : NNReal} : LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzOnWith.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {s : Set E} {a : E} {b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a - b‖ ≤ r) : ‖f a - f b‖ ≤ ↑C * r

theorem LipschitzOnWith.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {s : Set E} {a : E} {b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzOnWith C f s) (ha : a ∈ s) (hb : b ∈ s) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ ↑C * r

theorem lipschitzWith_iff_norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f ↔ ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem lipschitzWith_iff_norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

theorem LipschitzWith.norm_div_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f → ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Alias of the forward direction of lipschitzWith_iff_norm_div_le.

theorem LipschitzWith.norm_sub_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {C : NNReal} : LipschitzWith C f → ∀ (x y : E), ‖f x - f y‖ ≤ ↑C * ‖x - y‖

theorem LipschitzWith.norm_sub_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {a : E} {b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a - b‖ ≤ r) : ‖f a - f b‖ ≤ ↑C * r

theorem LipschitzWith.norm_div_le_of_le {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {a : E} {b : E} {r : ℝ} {f : E → F} {C : NNReal} (h : LipschitzWith C f) (hr : ‖a / b‖ ≤ r) : ‖f a / f b‖ ≤ ↑C * r

theorem AddMonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : Continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖

theorem MonoidHomClass.continuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : Continuous ⇑f

A homomorphism f of seminormed groups is continuous, if there exists a constant C such that for all x, one has ‖f x‖ ≤ C * ‖x‖.

theorem AddMonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : UniformContinuous ⇑f

theorem MonoidHomClass.uniformContinuous_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) : UniformContinuous ⇑f

theorem IsCompact.exists_bound_of_continuousOn {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E} (hf : ContinuousOn f s) : ∃ (C : ℝ), ∀ x ∈ s, ‖f x‖ ≤ C

theorem IsCompact.exists_bound_of_continuousOn' {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {s : Set α} (hs : IsCompact s) {f : α → E} (hf : ContinuousOn f s) : ∃ (C : ℝ), ∀ x ∈ s, ‖f x‖ ≤ C

theorem HasCompactSupport.exists_bound_of_continuous {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : HasCompactSupport f) (h'f : Continuous f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem HasCompactMulSupport.exists_bound_of_continuous {α : Type u_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem AddMonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem MonoidHomClass.isometry_iff_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖

theorem MonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f

Alias of the reverse direction of MonoidHomClass.isometry_iff_norm.

theorem AddMonoidHomClass.isometry_of_norm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) : (∀ (x : E), ‖f x‖ = ‖x‖) → Isometry ⇑f

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Alias of nndist_eq_nnnorm_sub.

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

Alias of nnnorm_le_nnnorm_add_nnnorm_sub'.

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

Alias of nnnorm_le_nnnorm_add_nnnorm_sub.

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

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

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

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

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

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

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

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

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

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

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

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

theorem AddMonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C ⇑f

theorem MonoidHomClass.lipschitz_of_bound_nnnorm {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal) (h : ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) : LipschitzWith C ⇑f

theorem AddMonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

theorem MonoidHomClass.antilipschitz_of_bound {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖) : AntilipschitzWith K ⇑f

theorem LipschitzWith.norm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖f x‖ ≤ ↑K * ‖x‖

theorem LipschitzWith.norm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖f x‖ ≤ ↑K * ‖x‖

theorem LipschitzWith.nnorm_le_mul {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖f x‖₊ ≤ K * ‖x‖₊

theorem LipschitzWith.nnorm_le_mul' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : LipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖f x‖₊ ≤ K * ‖x‖₊

theorem AntilipschitzWith.le_mul_norm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem AntilipschitzWith.le_mul_norm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem AntilipschitzWith.le_mul_nnnorm {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 0 = 0) (x : E) : ‖x‖₊ ≤ K * ‖f x‖₊

theorem AntilipschitzWith.le_mul_nnnorm' {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} {K : NNReal} (h : AntilipschitzWith K f) (hf : f 1 = 1) (x : E) : ‖x‖₊ ≤ K * ‖f x‖₊

theorem ZeroHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] [FunLike 𝓕 E F] [ZeroHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K ⇑f) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem OneHomClass.bound_of_antilipschitz {𝓕 : Type u_1} {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] [FunLike 𝓕 E F] [OneHomClass 𝓕 E F] (f : 𝓕) {K : NNReal} (h : AntilipschitzWith K ⇑f) (x : E) : ‖x‖ ≤ ↑K * ‖f x‖

theorem Isometry.nnnorm_map_of_map_zero {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 0 = 0) (x : E) : ‖f x‖₊ = ‖x‖₊

theorem Isometry.nnnorm_map_of_map_one {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) : ‖f x‖₊ = ‖x‖₊

theorem tendsto_iff_norm_sub_tendsto_zero {α : Type u_3} {E : Type u_6} [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_iff_norm_div_tendsto_zero {α : Type u_3} {E : Type u_6} [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_zero_iff_norm_tendsto_zero {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] {f : α → E} {a : Filter α} : Filter.Tendsto f a (nhds 0) ↔ Filter.Tendsto (fun (x : α) => ‖f x‖) a (nhds 0)

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

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

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

theorem squeeze_zero_norm' {α : Type u_3} {E : Type u_6} [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.PseudoMetric and Topology.Algebra.Order, the ' version is phrased using "eventually" and the non-' version is phrased absolutely.

theorem squeeze_one_norm' {α : Type u_3} {E : Type u_6} [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_3} {E : Type u_6} [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 squeeze_one_norm {α : Type u_3} {E : Type u_6} [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 tendsto_norm_sub_self {E : Type u_6} [SeminormedAddGroup E] (x : E) : Filter.Tendsto (fun (a : E) => ‖a - x‖) (nhds x) (nhds 0)

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

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

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

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

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

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

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

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

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

theorem lipschitzWith_one_norm {E : Type u_6} [SeminormedAddGroup E] : LipschitzWith 1 norm

theorem lipschitzWith_one_norm' {E : Type u_6} [SeminormedGroup E] : LipschitzWith 1 norm

theorem lipschitzWith_one_nnnorm {E : Type u_6} [SeminormedAddGroup E] : LipschitzWith 1 nnnorm

theorem lipschitzWith_one_nnnorm' {E : Type u_6} [SeminormedGroup E] : LipschitzWith 1 nnnorm

theorem uniformContinuous_norm {E : Type u_6} [SeminormedAddGroup E] : UniformContinuous norm

theorem uniformContinuous_norm' {E : Type u_6} [SeminormedGroup E] : UniformContinuous norm

theorem uniformContinuous_nnnorm {E : Type u_6} [SeminormedAddGroup E] : UniformContinuous fun (a : E) => ‖a‖₊

theorem uniformContinuous_nnnorm' {E : Type u_6} [SeminormedGroup E] : UniformContinuous fun (a : E) => ‖a‖₊

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

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

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

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

theorem Filter.Tendsto.op_zero_isBoundedUnder_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_one_isBoundedUnder_le' {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (h_op : ∃ (A : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖) : Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ A * ‖x‖ * ‖y‖ for some constant A instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_zero_isBoundedUnder_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedAddGroup E] [SeminormedAddGroup F] [SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Filter.Tendsto f l (nhds 0)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.op_one_isBoundedUnder_le {α : Type u_3} {E : Type u_6} {F : Type u_7} {G : Type u_8} [SeminormedGroup E] [SeminormedGroup F] [SeminormedGroup G] {f : α → E} {g : α → F} {l : Filter α} (hf : Filter.Tendsto f l (nhds 1)) (hg : Filter.IsBoundedUnder (fun (x x_1 : ℝ) => x ≤ x_1) l (norm ∘ g)) (op : E → F → G) (h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) : Filter.Tendsto (fun (x : α) => op (f x) (g x)) l (nhds 1)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to one and a bounded function tends to one. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

theorem Filter.Tendsto.norm {α : Type u_3} {E : Type u_6} [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.norm' {α : Type u_3} {E : Type u_6} [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_3} {E : Type u_6} [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_3} {E : Type u_6} [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 Continuous.norm {α : Type u_3} {E : Type u_6} [SeminormedAddGroup E] [TopologicalSpace α] {f : α → E} : Continuous f → Continuous fun (x : α) => ‖f x‖

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

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

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

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

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

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

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

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

theorem ContinuousWithinAt.norm' {α : Type u_3} {E : Type u_6} [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_3} {E : Type u_6} [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_3} {E : Type u_6} [SeminormedGroup E] [TopologicalSpace α] {f : α → E} {s : Set α} {a : α} (h : ContinuousWithinAt f s a) : ContinuousWithinAt (fun (x : α) => ‖f x‖₊) s a

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

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

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

theorem ContinuousOn.nnnorm' {α : Type u_3} {E : Type u_6} [SeminormedGroup 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_3} {E : Type u_6} [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 eventually_ne_of_tendsto_norm_atTop' {α : Type u_3} {E : Type u_6} [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 SeminormedAddCommGroup.mem_closure_iff {E : Type u_6} [SeminormedAddGroup E] {s : Set E} {a : E} : a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ s, ‖a - b‖ < ε

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

theorem norm_le_zero_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} : ‖a‖ ≤ 0 ↔ a = 0

theorem norm_le_zero_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} : ‖a‖ ≤ 0 ↔ a = 1

theorem norm_eq_zero' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} : ‖a‖ = 0 ↔ a = 0

theorem norm_eq_zero''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} : ‖a‖ = 0 ↔ a = 1

theorem norm_pos_iff' {E : Type u_6} [SeminormedAddGroup E] [T0Space E] {a : E} : 0 < ‖a‖ ↔ a ≠ 0

theorem norm_pos_iff''' {E : Type u_6} [SeminormedGroup E] [T0Space E] {a : E} : 0 < ‖a‖ ↔ a ≠ 1

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

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

theorem SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [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.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [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.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [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 SeminormedGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_one {ι : Type u_4} {κ : Type u_5} {G : Type u_8} [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

@[reducible]

def SeminormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := PseudoMetricSpace.induced (⇑f) SeminormedAddGroup.toPseudoMetricSpace; SeminormedAddGroup.mk ⋯

theorem SeminormedAddGroup.induced.proof_1 {𝓕 : Type u_3} (E : Type u_1) (F : Type u_2) [FunLike 𝓕 E F] [AddGroup E] [SeminormedAddGroup F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (x : E) (y : E) : dist x y = ‖x - y‖

@[reducible]

def SeminormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := PseudoMetricSpace.induced (⇑f) SeminormedGroup.toPseudoMetricSpace; SeminormedGroup.mk ⋯

theorem SeminormedAddCommGroup.induced.proof_1 (E : Type u_1) [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def SeminormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedAddGroup.induced E F f; SeminormedAddCommGroup.mk ⋯

@[reducible]

def SeminormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedGroup.induced E F f; SeminormedCommGroup.mk ⋯

@[reducible]

def NormedAddGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedAddGroup.induced E F f; let __src_1 := MetricSpace.induced (⇑f) h NormedAddGroup.toMetricSpace; NormedAddGroup.mk ⋯

@[reducible]

def NormedGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedGroup.induced E F f; let __src_1 := MetricSpace.induced (⇑f) h NormedGroup.toMetricSpace; NormedGroup.mk ⋯

@[reducible]

def NormedAddCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedAddGroup.induced E F f; let __src_1 := MetricSpace.induced (⇑f) h NormedAddGroup.toMetricSpace; NormedAddCommGroup.mk ⋯

theorem NormedAddCommGroup.induced.proof_1 (E : Type u_1) [AddCommGroup E] (a : E) (b : E) : a + b = b + a

@[reducible]

def NormedCommGroup.induced {𝓕 : Type u_1} (E : Type u_6) (F : Type u_7) [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 = let __src := SeminormedGroup.induced E F f; let __src_1 := MetricSpace.induced (⇑f) h NormedGroup.toMetricSpace; NormedCommGroup.mk ⋯

instance NormedAddGroup.to_isometricVAdd_left {E : Type u_6} [SeminormedAddCommGroup E] : IsometricVAdd E E

Equations

• ⋯ = ⋯

instance NormedGroup.to_isometricSMul_left {E : Type u_6} [SeminormedCommGroup E] : IsometricSMul E E

Equations

• ⋯ = ⋯

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

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

@[simp]

theorem dist_self_add_right {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) : dist a (a + b) = ‖b‖

@[simp]

theorem dist_self_mul_right {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) : dist a (a * b) = ‖b‖

@[simp]

theorem dist_self_add_left {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) : dist (a + b) a = ‖b‖

@[simp]

theorem dist_self_mul_left {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) : dist (a * b) a = ‖b‖

@[simp]

theorem dist_self_sub_right {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) : dist a (a - b) = ‖b‖

@[simp]

theorem dist_self_div_right {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) : dist a (a / b) = ‖b‖

@[simp]

theorem dist_self_sub_left {E : Type u_6} [SeminormedAddCommGroup E] (a : E) (b : E) : dist (a - b) a = ‖b‖

@[simp]

theorem dist_self_div_left {E : Type u_6} [SeminormedCommGroup E] (a : E) (b : E) : dist (a / b) a = ‖b‖

theorem dist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : dist (a₁ + a₂) (b₁ + b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_add_add_le_of_le {E : Type u_6} [SeminormedAddCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : ℝ} {r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ + a₂) (b₁ + b₂) ≤ r₁ + r₂

theorem dist_mul_mul_le_of_le {E : Type u_6} [SeminormedCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : ℝ} {r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂

theorem dist_sub_sub_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : dist (a₁ - a₂) (b₁ - b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_div_div_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂

theorem dist_sub_sub_le_of_le {E : Type u_6} [SeminormedAddCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : ℝ} {r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ - a₂) (b₁ - b₂) ≤ r₁ + r₂

theorem dist_div_div_le_of_le {E : Type u_6} [SeminormedCommGroup E] {a₁ : E} {a₂ : E} {b₁ : E} {b₂ : E} {r₁ : ℝ} {r₂ : ℝ} (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂

theorem abs_dist_sub_le_dist_add_add {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ + a₂) (b₁ + b₂)

theorem abs_dist_sub_le_dist_mul_mul {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂)

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

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

theorem norm_sum_le {ι : Type u_9} {E : Type u_10} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖Finset.sum s fun (i : ι) => f i‖ ≤ Finset.sum s fun (i : ι) => ‖f i‖

theorem norm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖Finset.prod s fun (i : ι) => f i‖ ≤ Finset.sum s fun (i : ι) => ‖f i‖

theorem norm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖Finset.sum s fun (b : ι) => f b‖ ≤ Finset.sum s fun (b : ι) => n b

theorem norm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → ℝ} (h : ∀ b ∈ s, ‖f b‖ ≤ n b) : ‖Finset.prod s fun (b : ι) => f b‖ ≤ Finset.sum s fun (b : ι) => n b

theorem dist_sum_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (Finset.sum s fun (b : ι) => f b) (Finset.sum s fun (b : ι) => a b) ≤ Finset.sum s fun (b : ι) => d b

theorem dist_prod_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) : dist (Finset.prod s fun (b : ι) => f b) (Finset.prod s fun (b : ι) => a b) ≤ Finset.sum s fun (b : ι) => d b

theorem dist_sum_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) (a : ι → E) : dist (Finset.sum s fun (b : ι) => f b) (Finset.sum s fun (b : ι) => a b) ≤ Finset.sum s fun (b : ι) => dist (f b) (a b)

theorem dist_prod_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) (a : ι → E) : dist (Finset.prod s fun (b : ι) => f b) (Finset.prod s fun (b : ι) => a b) ≤ Finset.sum s fun (b : ι) => dist (f b) (a b)

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem norm_nsmul_le {E : Type u_6} [SeminormedAddCommGroup E] (n : ℕ) (a : E) : ‖n • a‖ ≤ ↑n * ‖a‖

theorem norm_pow_le_mul_norm {E : Type u_6} [SeminormedCommGroup E] (n : ℕ) (a : E) : ‖a ^ n‖ ≤ ↑n * ‖a‖

theorem nnnorm_nsmul_le {E : Type u_6} [SeminormedAddCommGroup E] (n : ℕ) (a : E) : ‖n • a‖₊ ≤ ↑n * ‖a‖₊

theorem nnnorm_pow_le_mul_norm {E : Type u_6} [SeminormedCommGroup E] (n : ℕ) (a : E) : ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊

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

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

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

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

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

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

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

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

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

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

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

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

theorem controlled_sum_of_mem_closure {E : Type u_6} [SeminormedAddCommGroup E] {a : E} {s : AddSubgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) : ∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => 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 {E : Type u_6} [SeminormedCommGroup E] {a : E} {s : Subgroup E} (hg : a ∈ closure ↑s) {b : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < b n) : ∃ (v : ℕ → E), Filter.Tendsto (fun (n : ℕ) => Finset.prod (Finset.range (n + 1)) fun (i : ℕ) => 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_range {E : Type u_6} {F : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {j : E →+ F} {b : F} (hb : b ∈ closure ↑(AddMonoidHom.range j)) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) : ∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range (n + 1)) fun (i : ℕ) => j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) - b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

theorem controlled_prod_of_mem_closure_range {E : Type u_6} {F : Type u_7} [SeminormedCommGroup E] [SeminormedCommGroup F] {j : E →* F} {b : F} (hb : b ∈ closure ↑(MonoidHom.range j)) {f : ℕ → ℝ} (b_pos : ∀ (n : ℕ), 0 < f n) : ∃ (a : ℕ → E), Filter.Tendsto (fun (n : ℕ) => Finset.prod (Finset.range (n + 1)) fun (i : ℕ) => j (a i)) Filter.atTop (nhds b) ∧ ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

theorem nndist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : nndist (a₁ + a₂) (b₁ + b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

theorem nndist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂

theorem edist_add_add_le {E : Type u_6} [SeminormedAddCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : edist (a₁ + a₂) (b₁ + b₂) ≤ edist a₁ b₁ + edist a₂ b₂

theorem edist_mul_mul_le {E : Type u_6} [SeminormedCommGroup E] (a₁ : E) (a₂ : E) (b₁ : E) (b₂ : E) : edist (a₁ * a₂) (b₁ * b₂) ≤ edist a₁ b₁ + edist a₂ b₂

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

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

theorem nnnorm_sum_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E) : ‖Finset.sum s fun (a : ι) => f a‖₊ ≤ Finset.sum s fun (a : ι) => ‖f a‖₊

theorem nnnorm_prod_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) (f : ι → E) : ‖Finset.prod s fun (a : ι) => f a‖₊ ≤ Finset.sum s fun (a : ι) => ‖f a‖₊

theorem nnnorm_sum_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedAddCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖Finset.sum s fun (b : ι) => f b‖₊ ≤ Finset.sum s fun (b : ι) => n b

theorem nnnorm_prod_le_of_le {ι : Type u_4} {E : Type u_6} [SeminormedCommGroup E] (s : Finset ι) {f : ι → E} {n : ι → NNReal} (h : ∀ b ∈ s, ‖f b‖₊ ≤ n b) : ‖Finset.prod s fun (b : ι) => f b‖₊ ≤ Finset.sum s fun (b : ι) => 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‖

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

@[simp]

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

@[deprecated Real.norm_natCast]

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

Alias of Real.norm_natCast.

@[deprecated Real.nnnorm_natCast]

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

Alias of Real.nnnorm_natCast.

theorem Real.norm_two : ‖2‖ = 2

@[simp]

theorem Real.nnnorm_two : ‖2‖₊ = 2

theorem Real.nnnorm_of_nonneg {r : ℝ} (hr : 0 ≤ r) : ‖r‖₊ = { val := r, property := 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) : Real.toNNReal r = ‖r‖₊

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

instance Int.normedAddCommGroup : NormedAddCommGroup ℤ

Equations

• Int.normedAddCommGroup = NormedAddCommGroup.mk Int.normedAddCommGroup.proof_1

theorem Int.norm_cast_real (m : ℤ) : ‖↑m‖ = ‖m‖

theorem Int.norm_eq_abs (n : ℤ) : ‖n‖ = |↑n|

@[simp]

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

@[deprecated Int.norm_natCast]

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

Alias of Int.norm_natCast.

theorem NNReal.natCast_natAbs (n : ℤ) : ↑(Int.natAbs n) = ‖n‖₊

theorem Int.abs_le_floor_nnreal_iff (z : ℤ) (c : NNReal) : |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

instance Rat.normedAddCommGroup : NormedAddCommGroup ℚ

Equations

• Rat.normedAddCommGroup = NormedAddCommGroup.mk Rat.normedAddCommGroup.proof_1

@[simp]

theorem Rat.norm_cast_real (r : ℚ) : ‖↑r‖ = ‖r‖

@[simp]

theorem Int.norm_cast_rat (m : ℤ) : ‖↑m‖ = ‖m‖

theorem norm_zsmul_le {α : Type u_3} [SeminormedAddCommGroup α] (n : ℤ) (a : α) : ‖n • a‖ ≤ ‖n‖ * ‖a‖

theorem norm_zpow_le_mul_norm {α : Type u_3} [SeminormedCommGroup α] (n : ℤ) (a : α) : ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

theorem nnnorm_zsmul_le {α : Type u_3} [SeminormedAddCommGroup α] (n : ℤ) (a : α) : ‖n • a‖₊ ≤ ‖n‖₊ * ‖a‖₊

theorem nnnorm_zpow_le_mul_norm {α : Type u_3} [SeminormedCommGroup α] (n : ℤ) (a : α) : ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

theorem LipschitzWith.neg {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} (hf : LipschitzWith K f) : LipschitzWith K fun (x : α) => -f x

theorem LipschitzWith.inv {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {K : NNReal} {f : α → E} (hf : LipschitzWith K f) : LipschitzWith K fun (x : α) => (f x)⁻¹

theorem LipschitzWith.add {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x + g x

theorem LipschitzWith.mul' {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x * g x

theorem LipschitzWith.sub {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x - g x

theorem LipschitzWith.div {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (Kf + Kg) fun (x : α) => f x / g x

theorem AntilipschitzWith.add_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x + g x

theorem AntilipschitzWith.mul_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg g) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun (x : α) => f x * g x

theorem AntilipschitzWith.add_sub_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedAddCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g - f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

theorem AntilipschitzWith.mul_div_lipschitzWith {α : Type u_3} {E : Type u_6} [SeminormedCommGroup E] [PseudoEMetricSpace α] {Kf : NNReal} {Kg : NNReal} {f : α → E} {g : α → E} (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f)) (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

theorem AntilipschitzWith.le_mul_norm_sub {E : Type u_6} {F : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x : E) (y : E) : ‖x - y‖ ≤ ↑K * ‖f x - f y‖

theorem AntilipschitzWith.le_mul_norm_div {E : Type u_6} {F : Type u_7} [SeminormedCommGroup E] [SeminormedCommGroup F] {K : NNReal} {f : E → F} (hf : AntilipschitzWith K f) (x : E) (y : E) : ‖x / y‖ ≤ ↑K * ‖f x / f y‖

instance SeminormedAddCommGroup.to_lipschitzAdd {E : Type u_6} [SeminormedAddCommGroup E] : LipschitzAdd E

Equations

• ⋯ = ⋯

instance SeminormedCommGroup.to_lipschitzMul {E : Type u_6} [SeminormedCommGroup E] : LipschitzMul E

Equations

• ⋯ = ⋯

instance SeminormedAddCommGroup.to_uniformAddGroup {E : Type u_6} [SeminormedAddCommGroup E] : UniformAddGroup E

A seminormed group is a uniform additive group, i.e., addition and subtraction are uniformly continuous.

Equations

• ⋯ = ⋯

instance SeminormedCommGroup.to_uniformGroup {E : Type u_6} [SeminormedCommGroup E] : UniformGroup E

A seminormed group is a uniform group, i.e., multiplication and division are uniformly continuous.

Equations

• ⋯ = ⋯

instance SeminormedAddCommGroup.toTopologicalAddGroup {E : Type u_6} [SeminormedAddCommGroup E] : TopologicalAddGroup E

Equations

• ⋯ = ⋯

instance SeminormedCommGroup.toTopologicalGroup {E : Type u_6} [SeminormedCommGroup E] : TopologicalGroup E

Equations

• ⋯ = ⋯

theorem cauchySeq_sum_of_eventually_eq {E : Type u_6} [SeminormedAddCommGroup E] {u : ℕ → E} {v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => Finset.sum (Finset.range (n + 1)) fun (k : ℕ) => v k) : CauchySeq fun (n : ℕ) => Finset.sum (Finset.range (n + 1)) fun (k : ℕ) => u k

theorem cauchySeq_prod_of_eventually_eq {E : Type u_6} [SeminormedCommGroup E] {u : ℕ → E} {v : ℕ → E} {N : ℕ} (huv : ∀ n ≥ N, u n = v n) (hv : CauchySeq fun (n : ℕ) => Finset.prod (Finset.range (n + 1)) fun (k : ℕ) => v k) : CauchySeq fun (n : ℕ) => Finset.prod (Finset.range (n + 1)) fun (k : ℕ) => u k

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem eq_of_norm_div_eq_zero {E : Type u_6} [NormedGroup E] {a : E} {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_6} [NormedAddGroup E] {a : E} {b : E} : ‖a - b‖ = 0 → a = b

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem normAddGroupNorm.proof_1 (E : Type u_1) [NormedAddGroup E] : ∀ (x : E), ‖x‖ = 0 → x = 0

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

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

Equations

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

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

The norm of a normed group as a group norm.

Equations

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

@[simp]

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

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

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

Some relations with HasCompactSupport

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

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

Alias of the reverse direction of hasCompactSupport_norm_iff.

theorem Continuous.bounded_above_of_compact_support {α : Type u_3} {E : Type u_6} [NormedAddGroup E] [TopologicalSpace α] {f : α → E} (hf : Continuous f) (h : HasCompactSupport f) : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C

theorem HasCompactSupport.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [NormedAddGroup α] {f : α → E} [Zero E] (hf : HasCompactSupport f) : ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 0

theorem HasCompactMulSupport.exists_pos_le_norm {α : Type u_3} {E : Type u_6} [NormedAddGroup α] {f : α → E} [One E] (hf : HasCompactMulSupport f) : ∃ (R : ℝ), 0 < R ∧ ∀ (x : α), R ≤ ‖x‖ → f x = 1

ULift

instance ULift.norm {E : Type u_6} [Norm E] : Norm (ULift.{u_9, u_6} E)

Equations

• ULift.norm = { norm := fun (x : ULift.{u_9, u_6} E) => ‖x.down‖ }

theorem ULift.norm_def {E : Type u_6} [Norm E] (x : ULift.{u_9, u_6} E) : ‖x‖ = ‖x.down‖

@[simp]

theorem ULift.norm_up {E : Type u_6} [Norm E] (x : E) : ‖{ down := x }‖ = ‖x‖

@[simp]

theorem ULift.norm_down {E : Type u_6} [Norm E] (x : ULift.{u_9, u_6} E) : ‖x.down‖ = ‖x‖

instance ULift.nnnorm {E : Type u_6} [NNNorm E] : NNNorm (ULift.{u_9, u_6} E)

Equations

• ULift.nnnorm = { nnnorm := fun (x : ULift.{u_9, u_6} E) => ‖x.down‖₊ }

theorem ULift.nnnorm_def {E : Type u_6} [NNNorm E] (x : ULift.{u_9, u_6} E) : ‖x‖₊ = ‖x.down‖₊

@[simp]

theorem ULift.nnnorm_up {E : Type u_6} [NNNorm E] (x : E) : ‖{ down := x }‖₊ = ‖x‖₊

@[simp]

theorem ULift.nnnorm_down {E : Type u_6} [NNNorm E] (x : ULift.{u_9, u_6} E) : ‖x.down‖₊ = ‖x‖₊

theorem ULift.seminormedAddGroup.proof_1 {E : Type u_1} [SeminormedAddGroup E] : AddMonoidHomClass (ULift.{u_2, u_1} E →+ E) (ULift.{u_2, u_1} E) E

theorem ULift.seminormedAddGroup.proof_2 {E : Type u_1} [SeminormedAddGroup E] : 0.down = 0.down

theorem ULift.seminormedAddGroup.proof_3 {E : Type u_2} [SeminormedAddGroup E] : ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1)

instance ULift.seminormedAddGroup {E : Type u_6} [SeminormedAddGroup E] : SeminormedAddGroup (ULift.{u_9, u_6} E)

Equations

• ULift.seminormedAddGroup = SeminormedAddGroup.induced (ULift.{u_9, u_6} E) E { toZeroHom := { toFun := ULift.down, map_zero' := ⋯ }, map_add' := ⋯ }

instance ULift.seminormedGroup {E : Type u_6} [SeminormedGroup E] : SeminormedGroup (ULift.{u_9, u_6} E)

Equations

• ULift.seminormedGroup = SeminormedGroup.induced (ULift.{u_9, u_6} E) E { toOneHom := { toFun := ULift.down, map_one' := ⋯ }, map_mul' := ⋯ }

theorem ULift.seminormedAddCommGroup.proof_2 {E : Type u_1} [SeminormedAddCommGroup E] : 0.down = 0.down

instance ULift.seminormedAddCommGroup {E : Type u_6} [SeminormedAddCommGroup E] : SeminormedAddCommGroup (ULift.{u_9, u_6} E)

Equations

• ULift.seminormedAddCommGroup = SeminormedAddCommGroup.induced (ULift.{u_9, u_6} E) E { toZeroHom := { toFun := ULift.down, map_zero' := ⋯ }, map_add' := ⋯ }

theorem ULift.seminormedAddCommGroup.proof_3 {E : Type u_2} [SeminormedAddCommGroup E] : ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1)

theorem ULift.seminormedAddCommGroup.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] : AddMonoidHomClass (ULift.{u_2, u_1} E →+ E) (ULift.{u_2, u_1} E) E

instance ULift.seminormedCommGroup {E : Type u_6} [SeminormedCommGroup E] : SeminormedCommGroup (ULift.{u_9, u_6} E)

Equations

• ULift.seminormedCommGroup = SeminormedCommGroup.induced (ULift.{u_9, u_6} E) E { toOneHom := { toFun := ULift.down, map_one' := ⋯ }, map_mul' := ⋯ }

theorem ULift.normedAddGroup.proof_3 {E : Type u_2} [NormedAddGroup E] : ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1)

instance ULift.normedAddGroup {E : Type u_6} [NormedAddGroup E] : NormedAddGroup (ULift.{u_9, u_6} E)

Equations

• ULift.normedAddGroup = NormedAddGroup.induced (ULift.{u_9, u_6} E) E { toZeroHom := { toFun := ULift.down, map_zero' := ⋯ }, map_add' := ⋯ } ⋯

theorem ULift.normedAddGroup.proof_1 {E : Type u_1} [NormedAddGroup E] : AddMonoidHomClass (ULift.{u_2, u_1} E →+ E) (ULift.{u_2, u_1} E) E

theorem ULift.normedAddGroup.proof_2 {E : Type u_1} [NormedAddGroup E] : 0.down = 0.down

instance ULift.normedGroup {E : Type u_6} [NormedGroup E] : NormedGroup (ULift.{u_9, u_6} E)

Equations

• ULift.normedGroup = NormedGroup.induced (ULift.{u_9, u_6} E) E { toOneHom := { toFun := ULift.down, map_one' := ⋯ }, map_mul' := ⋯ } ⋯

theorem ULift.normedAddCommGroup.proof_1 {E : Type u_1} [NormedAddCommGroup E] : AddMonoidHomClass (ULift.{u_2, u_1} E →+ E) (ULift.{u_2, u_1} E) E

theorem ULift.normedAddCommGroup.proof_2 {E : Type u_1} [NormedAddCommGroup E] : 0.down = 0.down

theorem ULift.normedAddCommGroup.proof_3 {E : Type u_2} [NormedAddCommGroup E] : ∀ (x x_1 : ULift.{u_1, u_2} E), { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := ULift.down, map_zero' := ⋯ }.toFun (x + x_1)

instance ULift.normedAddCommGroup {E : Type u_6} [NormedAddCommGroup E] : NormedAddCommGroup (ULift.{u_9, u_6} E)

Equations

• ULift.normedAddCommGroup = NormedAddCommGroup.induced (ULift.{u_9, u_6} E) E { toZeroHom := { toFun := ULift.down, map_zero' := ⋯ }, map_add' := ⋯ } ⋯

instance ULift.normedCommGroup {E : Type u_6} [NormedCommGroup E] : NormedCommGroup (ULift.{u_9, u_6} E)

Equations

• ULift.normedCommGroup = NormedCommGroup.induced (ULift.{u_9, u_6} E) E { toOneHom := { toFun := ULift.down, map_one' := ⋯ }, map_mul' := ⋯ } ⋯

Additive, Multiplicative

instance Additive.toNorm {E : Type u_6} [Norm E] : Norm (Additive E)

Equations

• Additive.toNorm = inst

instance Multiplicative.toNorm {E : Type u_6} [Norm E] : Norm (Multiplicative E)

Equations

• Multiplicative.toNorm = inst

@[simp]

theorem norm_toMul {E : Type u_6} [Norm E] (x : Additive E) : ‖Additive.toMul x‖ = ‖x‖

@[simp]

theorem norm_ofMul {E : Type u_6} [Norm E] (x : E) : ‖Additive.ofMul x‖ = ‖x‖

@[simp]

theorem norm_toAdd {E : Type u_6} [Norm E] (x : Multiplicative E) : ‖Multiplicative.toAdd x‖ = ‖x‖

@[simp]

theorem norm_ofAdd {E : Type u_6} [Norm E] (x : E) : ‖Multiplicative.ofAdd x‖ = ‖x‖

instance Additive.toNNNorm {E : Type u_6} [NNNorm E] : NNNorm (Additive E)

Equations

• Additive.toNNNorm = inst

instance Multiplicative.toNNNorm {E : Type u_6} [NNNorm E] : NNNorm (Multiplicative E)

Equations

• Multiplicative.toNNNorm = inst

@[simp]

theorem nnnorm_toMul {E : Type u_6} [NNNorm E] (x : Additive E) : ‖Additive.toMul x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofMul {E : Type u_6} [NNNorm E] (x : E) : ‖Additive.ofMul x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_toAdd {E : Type u_6} [NNNorm E] (x : Multiplicative E) : ‖Multiplicative.toAdd x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofAdd {E : Type u_6} [NNNorm E] (x : E) : ‖Multiplicative.ofAdd x‖₊ = ‖x‖₊

instance Additive.seminormedAddGroup {E : Type u_6} [SeminormedGroup E] : SeminormedAddGroup (Additive E)

Equations

• Additive.seminormedAddGroup = SeminormedAddGroup.mk ⋯

instance Multiplicative.seminormedGroup {E : Type u_6} [SeminormedAddGroup E] : SeminormedGroup (Multiplicative E)

Equations

• Multiplicative.seminormedGroup = SeminormedGroup.mk ⋯

instance Additive.seminormedCommGroup {E : Type u_6} [SeminormedCommGroup E] : SeminormedAddCommGroup (Additive E)

Equations

• Additive.seminormedCommGroup = let __src := Additive.seminormedAddGroup; SeminormedAddCommGroup.mk ⋯

instance Multiplicative.seminormedAddCommGroup {E : Type u_6} [SeminormedAddCommGroup E] : SeminormedCommGroup (Multiplicative E)

Equations

• Multiplicative.seminormedAddCommGroup = let __src := Multiplicative.seminormedGroup; SeminormedCommGroup.mk ⋯

instance Additive.normedAddGroup {E : Type u_6} [NormedGroup E] : NormedAddGroup (Additive E)

Equations

• Additive.normedAddGroup = let __src := Additive.seminormedAddGroup; NormedAddGroup.mk ⋯

instance Multiplicative.normedGroup {E : Type u_6} [NormedAddGroup E] : NormedGroup (Multiplicative E)

Equations

• Multiplicative.normedGroup = let __src := Multiplicative.seminormedGroup; NormedGroup.mk ⋯

instance Additive.normedAddCommGroup {E : Type u_6} [NormedCommGroup E] : NormedAddCommGroup (Additive E)

Equations

• Additive.normedAddCommGroup = let __src := Additive.seminormedAddGroup; NormedAddCommGroup.mk ⋯

instance Multiplicative.normedCommGroup {E : Type u_6} [NormedAddCommGroup E] : NormedCommGroup (Multiplicative E)

Equations

• Multiplicative.normedCommGroup = let __src := Multiplicative.seminormedGroup; NormedCommGroup.mk ⋯

Order dual

instance OrderDual.toNorm {E : Type u_6} [Norm E] : Norm Eᵒᵈ

Equations

• OrderDual.toNorm = inst

@[simp]

theorem norm_toDual {E : Type u_6} [Norm E] (x : E) : ‖OrderDual.toDual x‖ = ‖x‖

@[simp]

theorem norm_ofDual {E : Type u_6} [Norm E] (x : Eᵒᵈ) : ‖OrderDual.ofDual x‖ = ‖x‖

instance OrderDual.toNNNorm {E : Type u_6} [NNNorm E] : NNNorm Eᵒᵈ

Equations

• OrderDual.toNNNorm = inst

@[simp]

theorem nnnorm_toDual {E : Type u_6} [NNNorm E] (x : E) : ‖OrderDual.toDual x‖₊ = ‖x‖₊

@[simp]

theorem nnnorm_ofDual {E : Type u_6} [NNNorm E] (x : Eᵒᵈ) : ‖OrderDual.ofDual x‖₊ = ‖x‖₊

instance OrderDual.seminormedAddGroup {E : Type u_6} [SeminormedAddGroup E] : SeminormedAddGroup Eᵒᵈ

Equations

• OrderDual.seminormedAddGroup = inst

instance OrderDual.seminormedGroup {E : Type u_6} [SeminormedGroup E] : SeminormedGroup Eᵒᵈ

Equations

• OrderDual.seminormedGroup = inst

instance OrderDual.seminormedAddCommGroup {E : Type u_6} [SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵒᵈ

Equations

• OrderDual.seminormedAddCommGroup = inst

instance OrderDual.seminormedCommGroup {E : Type u_6} [SeminormedCommGroup E] : SeminormedCommGroup Eᵒᵈ

Equations

• OrderDual.seminormedCommGroup = inst

instance OrderDual.normedAddGroup {E : Type u_6} [NormedAddGroup E] : NormedAddGroup Eᵒᵈ

Equations

• OrderDual.normedAddGroup = inst

instance OrderDual.normedGroup {E : Type u_6} [NormedGroup E] : NormedGroup Eᵒᵈ

Equations

• OrderDual.normedGroup = inst

instance OrderDual.normedAddCommGroup {E : Type u_6} [NormedAddCommGroup E] : NormedAddCommGroup Eᵒᵈ

Equations

• OrderDual.normedAddCommGroup = inst

instance OrderDual.normedCommGroup {E : Type u_6} [NormedCommGroup E] : NormedCommGroup Eᵒᵈ

Equations

• OrderDual.normedCommGroup = inst

Binary product of normed groups

instance Prod.toNorm {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] : Norm (E × F)

Equations

• Prod.toNorm = { norm := fun (x : E × F) => ‖x.1‖ ⊔ ‖x.2‖ }

theorem Prod.norm_def {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖

theorem norm_fst_le {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) : ‖x.1‖ ≤ ‖x‖

theorem norm_snd_le {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] (x : E × F) : ‖x.2‖ ≤ ‖x‖

theorem norm_prod_le_iff {E : Type u_6} {F : Type u_7} [Norm E] [Norm F] {x : E × F} {r : ℝ} : ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r

instance Prod.seminormedAddGroup {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] : SeminormedAddGroup (E × F)

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedAddGroup = SeminormedAddGroup.mk ⋯

theorem Prod.seminormedAddGroup.proof_1 {E : Type u_1} {F : Type u_2} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) (y : E × F) : max (dist x.1 y.1) (dist x.2 y.2) = max ‖x.1 - y.1‖ ‖x.2 - y.2‖

instance Prod.seminormedGroup {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] : SeminormedGroup (E × F)

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedGroup = SeminormedGroup.mk ⋯

theorem Prod.nnnorm_def' {E : Type u_6} {F : Type u_7} [SeminormedAddGroup E] [SeminormedAddGroup F] (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

theorem Prod.nnorm_def {E : Type u_6} {F : Type u_7} [SeminormedGroup E] [SeminormedGroup F] (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊

instance Prod.seminormedAddCommGroup {E : Type u_6} {F : Type u_7} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] : SeminormedAddCommGroup (E × F)

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedAddCommGroup = let __src := Prod.seminormedAddGroup; SeminormedAddCommGroup.mk ⋯

theorem Prod.seminormedAddCommGroup.proof_2 {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (x : E × F) (y : E × F) : dist x y = ‖x - y‖

theorem Prod.seminormedAddCommGroup.proof_1 {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] (a : E × F) (b : E × F) : a + b = b + a

instance Prod.seminormedCommGroup {E : Type u_6} {F : Type u_7} [SeminormedCommGroup E] [SeminormedCommGroup F] : SeminormedCommGroup (E × F)

Product of seminormed groups, using the sup norm.

Equations

• Prod.seminormedCommGroup = let __src := Prod.seminormedGroup; SeminormedCommGroup.mk ⋯

instance Prod.normedAddGroup {E : Type u_6} {F : Type u_7} [NormedAddGroup E] [NormedAddGroup F] : NormedAddGroup (E × F)

Product of normed groups, using the sup norm.

Equations

• Prod.normedAddGroup = let __src := Prod.seminormedAddGroup; NormedAddGroup.mk ⋯

theorem Prod.normedAddGroup.proof_2 {E : Type u_1} {F : Type u_2} [NormedAddGroup E] [NormedAddGroup F] (x : E × F) (y : E × F) : dist x y = ‖x - y‖

theorem Prod.normedAddGroup.proof_1 {E : Type u_1} {F : Type u_2} [NormedAddGroup E] [NormedAddGroup F] : ∀ {x y : E × F}, dist x y = 0 → x = y

instance Prod.normedGroup {E : Type u_6} {F : Type u_7} [NormedGroup E] [NormedGroup F] : NormedGroup (E × F)

Product of normed groups, using the sup norm.

Equations

• Prod.normedGroup = let __src := Prod.seminormedGroup; NormedGroup.mk ⋯

theorem Prod.normedAddCommGroup.proof_2 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] : ∀ {x y : E × F}, dist x y = 0 → x = y

theorem Prod.normedAddCommGroup.proof_1 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (a : E × F) (b : E × F) : a + b = b + a

theorem Prod.normedAddCommGroup.proof_3 {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (x : E × F) (y : E × F) : dist x y = ‖x - y‖

instance Prod.normedAddCommGroup {E : Type u_6} {F : Type u_7} [NormedAddCommGroup E] [NormedAddCommGroup F] : NormedAddCommGroup (E × F)

Product of normed groups, using the sup norm.

Equations

• Prod.normedAddCommGroup = let __src := Prod.seminormedAddGroup; NormedAddCommGroup.mk ⋯

instance Prod.normedCommGroup {E : Type u_6} {F : Type u_7} [NormedCommGroup E] [NormedCommGroup F] : NormedCommGroup (E × F)

Product of normed groups, using the sup norm.

Equations

• Prod.normedCommGroup = let __src := Prod.seminormedGroup; NormedCommGroup.mk ⋯

Finite product of normed groups

theorem Pi.seminormedAddGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) : ↑(Finset.sup Finset.univ fun (b : ι) => nndist (x b) (y b)) = ↑(Finset.sup Finset.univ fun (b : ι) => ‖(x - y) b‖₊)

instance Pi.seminormedAddGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] : SeminormedAddGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedAddGroup = SeminormedAddGroup.mk ⋯

instance Pi.seminormedGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] : SeminormedGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedGroup = SeminormedGroup.mk ⋯

theorem Pi.norm_def {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) : ‖f‖ = ↑(Finset.sup Finset.univ fun (b : ι) => ‖f b‖₊)

theorem Pi.norm_def' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) : ‖f‖ = ↑(Finset.sup Finset.univ fun (b : ι) => ‖f b‖₊)

theorem Pi.nnnorm_def {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) : ‖f‖₊ = Finset.sup Finset.univ fun (b : ι) => ‖f b‖₊

theorem Pi.nnnorm_def' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) : ‖f‖₊ = Finset.sup Finset.univ fun (b : ι) => ‖f b‖₊

theorem pi_norm_le_iff_of_nonneg {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : ℝ} (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

theorem pi_norm_le_iff_of_nonneg' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : ℝ} (hr : 0 ≤ r) : ‖x‖ ≤ r ↔ ∀ (i : ι), ‖x i‖ ≤ r

The seminorm of an element in a product space is ≤ r if and only if the norm of each component is.

theorem pi_nnnorm_le_iff {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} : ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

theorem pi_nnnorm_le_iff' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} : ‖x‖₊ ≤ r ↔ ∀ (i : ι), ‖x i‖₊ ≤ r

theorem pi_norm_le_iff_of_nonempty {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) {r : ℝ} [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

theorem pi_norm_le_iff_of_nonempty' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) {r : ℝ} [Nonempty ι] : ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

theorem pi_norm_lt_iff {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : ℝ} (hr : 0 < r) : ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

theorem pi_norm_lt_iff' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : ℝ} (hr : 0 < r) : ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

The seminorm of an element in a product space is < r if and only if the norm of each component is.

theorem pi_nnnorm_lt_iff {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

theorem pi_nnnorm_lt_iff' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] {x : (i : ι) → π i} {r : NNReal} (hr : 0 < r) : ‖x‖₊ < r ↔ ∀ (i : ι), ‖x i‖₊ < r

theorem norm_le_pi_norm {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) : ‖f i‖ ≤ ‖f‖

theorem norm_le_pi_norm' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) : ‖f i‖ ≤ ‖f‖

theorem nnnorm_le_pi_nnnorm {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) (i : ι) : ‖f i‖₊ ≤ ‖f‖₊

theorem nnnorm_le_pi_nnnorm' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) (i : ι) : ‖f i‖₊ ≤ ‖f‖₊

theorem pi_norm_const_le {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] (a : E) : ‖fun (x : ι) => a‖ ≤ ‖a‖

theorem pi_norm_const_le' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] (a : E) : ‖fun (x : ι) => a‖ ≤ ‖a‖

theorem pi_nnnorm_const_le {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] (a : E) : ‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

theorem pi_nnnorm_const_le' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] (a : E) : ‖fun (x : ι) => a‖₊ ≤ ‖a‖₊

@[simp]

theorem pi_norm_const {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖ = ‖a‖

@[simp]

theorem pi_norm_const' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖ = ‖a‖

@[simp]

theorem pi_nnnorm_const {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedAddGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖₊ = ‖a‖₊

@[simp]

theorem pi_nnnorm_const' {ι : Type u_4} {E : Type u_6} [Fintype ι] [SeminormedGroup E] [Nonempty ι] (a : E) : ‖fun (_i : ι) => a‖₊ = ‖a‖₊

theorem Pi.sum_norm_apply_le_norm {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) : (Finset.sum Finset.univ fun (i : ι) => ‖f i‖) ≤ Fintype.card ι • ‖f‖

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_norm_apply_le_norm' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) : (Finset.sum Finset.univ fun (i : ι) => ‖f i‖) ≤ Fintype.card ι • ‖f‖

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_nnnorm_apply_le_nnnorm {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddGroup (π i)] (f : (i : ι) → π i) : (Finset.sum Finset.univ fun (i : ι) => ‖f i‖₊) ≤ Fintype.card ι • ‖f‖₊

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.sum_nnnorm_apply_le_nnnorm' {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedGroup (π i)] (f : (i : ι) → π i) : (Finset.sum Finset.univ fun (i : ι) => ‖f i‖₊) ≤ Fintype.card ι • ‖f‖₊

The $L^1$ norm is less than the $L^\infty$ norm scaled by the cardinality.

theorem Pi.seminormedAddCommGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) : dist x y = ‖x - y‖

instance Pi.seminormedAddCommGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedAddCommGroup (π i)] : SeminormedAddCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedAddCommGroup = let __src := Pi.seminormedAddGroup; SeminormedAddCommGroup.mk ⋯

theorem Pi.seminormedAddCommGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → SeminormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) : a + b = b + a

instance Pi.seminormedCommGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → SeminormedCommGroup (π i)] : SeminormedCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.seminormedCommGroup = let __src := Pi.seminormedGroup; SeminormedCommGroup.mk ⋯

theorem Pi.normedAddGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) : dist x y = ‖x - y‖

theorem Pi.normedAddGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] : ∀ {x y : (i : ι) → π i}, dist x y = 0 → x = y

instance Pi.normedAddGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → NormedAddGroup (π i)] : NormedAddGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.normedAddGroup = let __src := Pi.seminormedAddGroup; NormedAddGroup.mk ⋯

instance Pi.normedGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → NormedGroup (π i)] : NormedGroup ((i : ι) → π i)

Finite product of normed groups, using the sup norm.

Equations

• Pi.normedGroup = let __src := Pi.seminormedGroup; NormedGroup.mk ⋯

theorem Pi.normedAddCommGroup.proof_3 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] (x : (i : ι) → π i) (y : (i : ι) → π i) : dist x y = ‖x - y‖

theorem Pi.normedAddCommGroup.proof_2 {ι : Type u_1} {π : ι → Type u_2} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] : ∀ {x y : (i : ι) → π i}, dist x y = 0 → x = y

theorem Pi.normedAddCommGroup.proof_1 {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → NormedAddCommGroup (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) : a + b = b + a

instance Pi.normedAddCommGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → NormedAddCommGroup (π i)] : NormedAddCommGroup ((i : ι) → π i)

Finite product of seminormed groups, using the sup norm.

Equations

• Pi.normedAddCommGroup = let __src := Pi.seminormedAddGroup; NormedAddCommGroup.mk ⋯

instance Pi.normedCommGroup {ι : Type u_4} {π : ι → Type u_9} [Fintype ι] [(i : ι) → NormedCommGroup (π i)] : NormedCommGroup ((i : ι) → π i)

Finite product of normed groups, using the sup norm.

Equations

• Pi.normedCommGroup = let __src := Pi.seminormedGroup; NormedCommGroup.mk ⋯

Multiplicative opposite

instance MulOpposite.instSeminormedAddGroup {E : Type u_6} [SeminormedAddGroup E] : SeminormedAddGroup Eᵐᵒᵖ

The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

Note that we do not provide this more generally as Norm Eᵐᵒᵖ, as this is not always a good choice of norm in the multiplicative SeminormedGroup E case.

We could repeat this instance to provide a [SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ instance, but that case would likely never be used.

Equations

• MulOpposite.instSeminormedAddGroup = let __spread.0 := MulOpposite.instPseudoMetricSpace; SeminormedAddGroup.mk ⋯

theorem MulOpposite.norm_op {E : Type u_6} [SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖ = ‖a‖

theorem MulOpposite.norm_unop {E : Type u_6} [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖ = ‖a‖

theorem MulOpposite.nnnorm_op {E : Type u_6} [SeminormedAddGroup E] (a : E) : ‖MulOpposite.op a‖₊ = ‖a‖₊

theorem MulOpposite.nnnorm_unop {E : Type u_6} [SeminormedAddGroup E] (a : Eᵐᵒᵖ) : ‖MulOpposite.unop a‖₊ = ‖a‖₊

instance MulOpposite.instNormedAddGroup {E : Type u_6} [NormedAddGroup E] : NormedAddGroup Eᵐᵒᵖ

Equations

• MulOpposite.instNormedAddGroup = let __spread.0 := MulOpposite.instMetricSpace; let __spread.1 := MulOpposite.instSeminormedAddGroup; NormedAddGroup.mk ⋯

instance MulOpposite.instSeminormedAddCommGroup {E : Type u_6} [SeminormedAddCommGroup E] : SeminormedAddCommGroup Eᵐᵒᵖ

Equations

• MulOpposite.instSeminormedAddCommGroup = SeminormedAddCommGroup.mk ⋯

instance MulOpposite.instNormedAddCommGroup {E : Type u_6} [NormedAddCommGroup E] : NormedAddCommGroup Eᵐᵒᵖ

Equations

• MulOpposite.instNormedAddCommGroup = let __spread.0 := MulOpposite.instSeminormedAddCommGroup; let __spread.1 := MulOpposite.instNormedAddGroup; NormedAddCommGroup.mk ⋯

Subgroups of normed groups

instance AddSubgroup.seminormedAddGroup {E : Type u_6} [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 (AddSubgroup.subtype s)

theorem AddSubgroup.seminormedAddGroup.proof_1 {E : Type u_1} [SeminormedAddGroup E] {s : AddSubgroup E} : AddMonoidHomClass (↥s →+ E) (↥s) E

instance Subgroup.seminormedGroup {E : Type u_6} [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 (Subgroup.subtype s)

@[simp]

theorem AddSubgroup.coe_norm {E : Type u_6} [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.

@[simp]

theorem Subgroup.coe_norm {E : Type u_6} [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.

theorem AddSubgroup.norm_coe {E : Type u_6} [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.

theorem Subgroup.norm_coe {E : Type u_6} [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.seminormedAddCommGroup.proof_1 {E : Type u_1} [SeminormedAddCommGroup E] {s : AddSubgroup E} : AddMonoidHomClass (↥s →+ E) (↥s) E

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

Equations

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

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

Equations

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

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

Equations

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

theorem AddSubgroup.normedAddGroup.proof_2 {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} : Function.Injective fun (a : ↥s) => ↑a

theorem AddSubgroup.normedAddGroup.proof_1 {E : Type u_1} [NormedAddGroup E] {s : AddSubgroup E} : AddMonoidHomClass (↥s →+ E) (↥s) E

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

Equations

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

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

Equations

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

theorem AddSubgroup.normedAddCommGroup.proof_2 {E : Type u_1} [NormedAddCommGroup E] {s : AddSubgroup E} : Function.Injective fun (a : ↥s) => ↑a

theorem AddSubgroup.normedAddCommGroup.proof_1 {E : Type u_1} [NormedAddCommGroup E] {s : AddSubgroup E} : AddMonoidHomClass (↥s →+ E) (↥s) E

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

Equations

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

Submodules of normed groups

instance Submodule.seminormedAddCommGroup {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : SeminormedAddCommGroup ↥s

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

Equations

• Submodule.seminormedAddCommGroup s = SeminormedAddCommGroup.induced (↥s) E (LinearMap.toAddMonoidHom (Submodule.subtype s))

@[simp]

theorem Submodule.coe_norm {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : ↥s) : ‖x‖ = ‖↑x‖

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

theorem Submodule.norm_coe {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] {s : Submodule 𝕜 E} (x : ↥s) : ‖↑x‖ = ‖x‖

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

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

instance Submodule.normedAddCommGroup {𝕜 : Type u_2} {E : Type u_6} [Ring 𝕜] [NormedAddCommGroup E] [Module 𝕜 E] (s : Submodule 𝕜 E) : NormedAddCommGroup ↥s

A submodule of a normed group is also a normed group, with the restriction of the norm.

Equations

• Submodule.normedAddCommGroup s = let __src := Submodule.seminormedAddCommGroup s; NormedAddCommGroup.mk ⋯