Ordered normed spaces

In this file, we define classes for fields and groups that are both normed and ordered. These are mostly useful to avoid diamonds during type class inference.

@[deprecated "Use `[NormedAddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure NormedOrderedAddGroup (α : Type u_2) extends OrderedAddCommGroup α, Norm α, MetricSpace α : Type u_2

A NormedOrderedAddGroup is an additive group that is both a NormedAddCommGroup and an OrderedAddCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

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

  The distance function is induced by the norm.

@[deprecated "Use `[NormedCommGroup α] [PartialOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure NormedOrderedGroup (α : Type u_2) extends OrderedCommGroup α, Norm α, MetricSpace α : Type u_2

A NormedOrderedGroup is a group that is both a NormedCommGroup and an OrderedCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

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

  The distance function is induced by the norm.

@[deprecated "Use `[NormedAddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure NormedLinearOrderedAddGroup (α : Type u_2) extends LinearOrderedAddCommGroup α, Norm α, MetricSpace α : Type u_2

A NormedLinearOrderedAddGroup is an additive group that is both a NormedAddCommGroup and a LinearOrderedAddCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• norm : α → ℝ
• dist : α → α → ℝ
• dist_self (x : α) : dist x x = 0
• dist_comm (x y : α) : dist x y = dist y x
• dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

@[deprecated "Use `[NormedCommGroup α] [LinearOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure NormedLinearOrderedGroup (α : Type u_2) extends LinearOrderedCommGroup α, Norm α, MetricSpace α : Type u_2

A NormedLinearOrderedGroup is a group that is both a NormedCommGroup and a LinearOrderedCommGroup. This class is necessary to avoid diamonds caused by both classes carrying their own group structure.

• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : α) : a⁻¹ * a = 1
• mul_comm (a b : α) : a * b = b * a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• norm : α → ℝ
• dist : α → α → ℝ
• dist_self (x : α) : dist x x = 0
• dist_comm (x y : α) : dist x y = dist y x
• dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x / y‖

  The distance function is induced by the norm.

@[deprecated "Use `[NormedField α] [LinearOrder α] [IsStrictOrderedRing α]` instead." (since := "2025-04-10")]

structure NormedLinearOrderedField (α : Type u_2) extends LinearOrderedField α, Norm α, MetricSpace α : Type u_2

A NormedLinearOrderedField is a field that is both a NormedField and a LinearOrderedField. This class is necessary to avoid diamonds.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos (a b : α) : 0 < a → 0 < b → 0 < a * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• mul_comm (a b : α) : a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : self.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : self.zpow (↑n.succ) a = self.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : self.zpow (Int.negSucc n) a = (self.zpow (↑n.succ) a)⁻¹
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel (a : α) : a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def (q : ℚ≥0) (a : α) : self.nnqsmul q a = ↑q * a
• ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def (a : ℚ) (x : α) : self.qsmul a x = ↑a * x
• norm : α → ℝ
• dist : α → α → ℝ
• dist_self (x : α) : dist x x = 0
• dist_comm (x y : α) : dist x y = dist y x
• dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : α} : dist x y = 0 → x = y
• dist_eq (x y : α) : dist x y = ‖x - y‖

  The distance function is induced by the norm.

• norm_mul (x y : α) : ‖x * y‖ = ‖x‖ * ‖y‖

  The norm is multiplicative.