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.

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

• 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 = x + AddMonoid.nsmul n 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 (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_le : ∀ (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 : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → 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.

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.

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

• 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 = x * Monoid.npow n 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 (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : α), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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_le : ∀ (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 : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → 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.

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.

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

• 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 = x + AddMonoid.nsmul n 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 (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_le : ∀ (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
• decidableLE : DecidableRel fun x x_1 => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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 : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → 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.

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.

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

• 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 = x * Monoid.npow n 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 (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : α), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (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_le : ∀ (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
• decidableLE : DecidableRel fun x x_1 => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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 : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → 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.

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.

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (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_le : ∀ (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
• decidableLE : DecidableRel fun x x_1 => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max 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 : α), LinearOrderedField.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.ofNat (Nat.succ n)) a = a * LinearOrderedField.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑(Nat.succ n)) a)⁻¹
• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹
• qsmul : ℚ → α → α
• qsmul_eq_mul' : ∀ (a : ℚ) (x : α), LinearOrderedField.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 : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → 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.

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

instance NormedOrderedAddGroup.toNormedAddCommGroup {α : Type u_1} [NormedOrderedAddGroup α] : NormedAddCommGroup α

Equations

• NormedOrderedAddGroup.toNormedAddCommGroup = NormedAddCommGroup.mk

instance NormedOrderedGroup.toNormedCommGroup {α : Type u_1} [NormedOrderedGroup α] : NormedCommGroup α

Equations

• NormedOrderedGroup.toNormedCommGroup = NormedCommGroup.mk

instance NormedLinearOrderedAddGroup.toNormedOrderedAddGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] : NormedOrderedAddGroup α

Equations

• NormedLinearOrderedAddGroup.toNormedOrderedAddGroup = NormedOrderedAddGroup.mk

instance NormedLinearOrderedGroup.toNormedOrderedGroup {α : Type u_1} [NormedLinearOrderedGroup α] : NormedOrderedGroup α

Equations

• NormedLinearOrderedGroup.toNormedOrderedGroup = NormedOrderedGroup.mk

instance NormedLinearOrderedField.toNormedField (α : Type u_2) [NormedLinearOrderedField α] : NormedField α

Equations

• NormedLinearOrderedField.toNormedField α = NormedField.mk (_ : ∀ (x y : α), dist x y = ‖x - y‖) (_ : ∀ (x y : α), ‖x * y‖ = ‖x‖ * ‖y‖)

instance Rat.normedLinearOrderedField : NormedLinearOrderedField ℚ

Equations

• Rat.normedLinearOrderedField = NormedLinearOrderedField.mk Rat.normedLinearOrderedField.proof_2

noncomputable instance Real.normedLinearOrderedField : NormedLinearOrderedField ℝ

Equations

• Real.normedLinearOrderedField = NormedLinearOrderedField.mk Real.normedLinearOrderedField.proof_2

instance OrderDual.normedOrderedAddGroup {α : Type u_1} [NormedOrderedAddGroup α] : NormedOrderedAddGroup αᵒᵈ

Equations

• OrderDual.normedOrderedAddGroup = let src := NormedOrderedAddGroup.toNormedAddCommGroup; let src_1 := OrderDual.orderedAddCommGroup; NormedOrderedAddGroup.mk

theorem OrderDual.normedOrderedAddGroup.proof_1 {α : Type u_1} [NormedOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b → ∀ (c : αᵒᵈ), c + a ≤ c + b

instance OrderDual.normedOrderedGroup {α : Type u_1} [NormedOrderedGroup α] : NormedOrderedGroup αᵒᵈ

Equations

• OrderDual.normedOrderedGroup = let src := NormedOrderedGroup.toNormedCommGroup; let src_1 := OrderDual.orderedCommGroup; NormedOrderedGroup.mk

theorem OrderDual.normedLinearOrderedAddGroup.proof_5 {α : Type u_1} [NormedLinearOrderedAddGroup α] (x : αᵒᵈ) (y : αᵒᵈ) : dist x y = ‖x - y‖

theorem OrderDual.normedLinearOrderedAddGroup.proof_4 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : compare a b = compareOfLessAndEq a b

theorem OrderDual.normedLinearOrderedAddGroup.proof_2 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : min a b = if a ≤ b then a else b

instance OrderDual.normedLinearOrderedAddGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] : NormedLinearOrderedAddGroup αᵒᵈ

Equations

• OrderDual.normedLinearOrderedAddGroup = let src := OrderDual.normedOrderedAddGroup; let src_1 := OrderDual.instLinearOrder α; NormedLinearOrderedAddGroup.mk

theorem OrderDual.normedLinearOrderedAddGroup.proof_3 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : max a b = if a ≤ b then b else a

theorem OrderDual.normedLinearOrderedAddGroup.proof_1 {α : Type u_1} [NormedLinearOrderedAddGroup α] (a : αᵒᵈ) (b : αᵒᵈ) : a ≤ b ∨ b ≤ a

instance OrderDual.normedLinearOrderedGroup {α : Type u_1} [NormedLinearOrderedGroup α] : NormedLinearOrderedGroup αᵒᵈ

Equations

• OrderDual.normedLinearOrderedGroup = let src := OrderDual.normedOrderedGroup; let src_1 := OrderDual.instLinearOrder α; NormedLinearOrderedGroup.mk

instance Additive.normedOrderedAddGroup {α : Type u_1} [NormedOrderedGroup α] : NormedOrderedAddGroup (Additive α)

Equations

• Additive.normedOrderedAddGroup = let src := Additive.normedAddCommGroup; let src_1 := Additive.orderedAddCommGroup; NormedOrderedAddGroup.mk

instance Multiplicative.normedOrderedGroup {α : Type u_1} [NormedOrderedAddGroup α] : NormedOrderedGroup (Multiplicative α)

Equations

• Multiplicative.normedOrderedGroup = let src := Multiplicative.normedCommGroup; let src_1 := Multiplicative.orderedCommGroup; NormedOrderedGroup.mk

instance Additive.normedLinearOrderedAddGroup {α : Type u_1} [NormedLinearOrderedGroup α] : NormedLinearOrderedAddGroup (Additive α)

Equations

• Additive.normedLinearOrderedAddGroup = let src := Additive.normedAddCommGroup; let src_1 := Additive.linearOrderedAddCommGroup; NormedLinearOrderedAddGroup.mk

instance Multiplicative.normedlinearOrderedGroup {α : Type u_1} [NormedLinearOrderedAddGroup α] : NormedLinearOrderedGroup (Multiplicative α)

Equations

• Multiplicative.normedlinearOrderedGroup = let src := Multiplicative.normedCommGroup; let src_1 := Multiplicative.linearOrderedCommGroup; NormedLinearOrderedGroup.mk