(Semi)normed groups: definitions

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 provide some instances relating these classes.

Notes

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

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

Tags

normed group

class Norm (E : Type u_8) : Type u_8

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

• norm : E → ℝ

  the ℝ-valued norm function.

class NNNorm (E : Type u_8) : Type u_8

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

• nnnorm : E → NNReal

  the ℝ≥0-valued norm function.

class ENorm (E : Type u_8) : Type u_8

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

• enorm : E → ENNReal

  the ℝ≥0∞-valued norm function.

def «term‖_‖» : Lean.ParserDescr

the ℝ-valued norm function.

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

the ℝ≥0-valued norm function.

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

the ℝ≥0∞-valued norm function.

instance NNNorm.toENorm {E : Type u_8} [NNNorm E] : ENorm E

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

@[simp]

theorem toNNReal_enorm {E : Type u_8} [NNNorm E] (x : E) : ‖x‖ₑ.toNNReal = ‖x‖₊

@[simp]

theorem coe_le_enorm {E : Type u_8} [NNNorm E] {x : E} {r : NNReal} : ↑r ≤ ‖x‖ₑ ↔ r ≤ ‖x‖₊

@[simp]

theorem enorm_le_coe {E : Type u_8} [NNNorm E] {x : E} {r : NNReal} : ‖x‖ₑ ≤ ↑r ↔ ‖x‖₊ ≤ r

@[simp]

theorem coe_lt_enorm {E : Type u_8} [NNNorm E] {x : E} {r : NNReal} : ↑r < ‖x‖ₑ ↔ r < ‖x‖₊

@[simp]

theorem enorm_lt_coe {E : Type u_8} [NNNorm E] {x : E} {r : NNReal} : ‖x‖ₑ < ↑r ↔ ‖x‖₊ < r

@[simp]

theorem enorm_ne_top {E : Type u_8} [NNNorm E] {x : E} : ‖x‖ₑ ≠ ⊤

@[simp]

theorem enorm_lt_top {E : Type u_8} [NNNorm E] {x : E} : ‖x‖ₑ < ⊤

class ContinuousENorm (E : Type u_8) [TopologicalSpace E] extends ENorm E : Type u_8

A type E equipped with a continuous map ‖·‖ₑ : E → ℝ≥0∞

NB. We do not demand that the topology is somehow defined by the enorm: for ℝ≥0∞ (the motivating example behind this definition), this is not true.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm

class ESeminormedAddMonoid (E : Type u_8) [TopologicalSpace E] extends ContinuousENorm E, AddMonoid E : Type u_8

An e-seminormed monoid is an additive monoid endowed with a continuous enorm. Note that we do not ask for the enorm to be positive definite: non-trivial elements may have enorm zero.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

class ENormedAddMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedAddMonoid E : Type u_8

An enormed monoid is an additive monoid endowed with a continuous enorm, which is positive definite: in other words, this is an ESeminormedAddMonoid with a positive definiteness condition added.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0

class ESeminormedMonoid (E : Type u_8) [TopologicalSpace E] extends ContinuousENorm E, Monoid E : Type u_8

An e-seminormed monoid is a monoid endowed with a continuous enorm. Note that we only ask for the enorm to be a semi-norm: non-trivial elements may have enorm zero.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖1‖ₑ = 0
• enorm_mul_le (x y : E) : ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ

class ENormedMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedMonoid E : Type u_8

An enormed monoid is a monoid endowed with a continuous enorm, which is positive definite: in other words, this is an ESeminormedMonoid with a positive definiteness condition added.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖1‖ₑ = 0
• enorm_mul_le (x y : E) : ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 1

class ESeminormedAddCommMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedAddMonoid E, AddCommMonoid E : Type u_8

An e-seminormed commutative monoid is an additive commutative monoid endowed with a continuous enorm.

We don't have ESeminormedAddCommMonoid extend EMetricSpace, since the canonical instance ℝ≥0∞ is not an EMetricSpace. This is because ℝ≥0∞ carries the order topology, which is distinct from the topology coming from edist.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a

class ENormedAddCommMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedAddCommMonoid E, ENormedAddMonoid E : Type u_8

An enormed commutative monoid is an additive commutative monoid endowed with a continuous enorm which is positive definite.

We don't have ENormedAddCommMonoid extend EMetricSpace, since the canonical instance ℝ≥0∞ is not an EMetricSpace. This is because ℝ≥0∞ carries the order topology, which is distinct from the topology coming from edist.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖0‖ₑ = 0
• enorm_add_le (x y : E) : ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• add_comm (a b : E) : a + b = b + a
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 0

class ESeminormedCommMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedMonoid E, CommMonoid E : Type u_8

An e-seminormed commutative monoid is a commutative monoid endowed with a continuous enorm.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖1‖ₑ = 0
• enorm_mul_le (x y : E) : ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• mul_comm (a b : E) : a * b = b * a

class ENormedCommMonoid (E : Type u_8) [TopologicalSpace E] extends ESeminormedCommMonoid E, ENormedMonoid E : Type u_8

An enormed commutative monoid is a commutative monoid endowed with a continuous enorm which is positive definite.

• enorm : E → ENNReal
• continuous_enorm : Continuous enorm
• 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
• enorm_zero : ‖1‖ₑ = 0
• enorm_mul_le (x y : E) : ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
• mul_comm (a b : E) : a * b = b * a
• enorm_eq_zero (x : E) : ‖x‖ₑ = 0 ↔ x = 1

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

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

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

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

  The distance function is induced by the norm.

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[instance 100]

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

Construct a seminormed group from a multiplication-invariant distance.

@[reducible, inline]

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

Construct a seminormed group from a translation-invariant distance.

@[reducible, inline]

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

Construct a seminormed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a seminormed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

Construct a seminormed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a seminormed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

Construct a seminormed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a seminormed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a multiplication-invariant distance.

@[reducible, inline]

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

Construct a normed group from a translation-invariant distance.

@[reducible, inline]

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

Construct a normed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a multiplication-invariant pseudodistance.

@[reducible, inline]

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

Construct a normed group from a translation-invariant pseudodistance.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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