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

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_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.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.

class 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_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.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.

class 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_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 (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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 : α), PseudoMetricSpace.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.

class 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_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 (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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 : α), PseudoMetricSpace.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.

class 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 : 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 = 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_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 (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• 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 : α), LinearOrderedField.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (↑n.succ) a = LinearOrderedField.zpow (↑n) a * a
• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.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 : α), LinearOrderedField.nnqsmul q a = ↑q * a
• ratCast_def : ∀ (q : ℚ), ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def : ∀ (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.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.

@[instance 100]

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

Equations

• NormedOrderedGroup.toNormedCommGroup = NormedCommGroup.mk ⋯

@[instance 100]

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

Equations

• NormedOrderedAddGroup.toNormedAddCommGroup = NormedAddCommGroup.mk ⋯

@[instance 100]

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

Equations

• NormedLinearOrderedGroup.toNormedOrderedGroup = NormedOrderedGroup.mk ⋯

@[instance 100]

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

Equations

• NormedLinearOrderedAddGroup.toNormedOrderedAddGroup = NormedOrderedAddGroup.mk ⋯

@[instance 100]

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

Equations

• NormedLinearOrderedField.toNormedField α = NormedField.mk ⋯ ⋯

instance Rat.normedLinearOrderedField : NormedLinearOrderedField ℚ

Equations

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

noncomputable instance Real.normedLinearOrderedField : NormedLinearOrderedField ℝ

Equations

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

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

Equations

• OrderDual.normedOrderedGroup = NormedOrderedGroup.mk ⋯

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

Equations

• OrderDual.normedOrderedAddGroup = NormedOrderedAddGroup.mk ⋯

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

Equations

• OrderDual.normedLinearOrderedGroup = NormedLinearOrderedGroup.mk ⋯

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

Equations

• OrderDual.normedLinearOrderedAddGroup = NormedLinearOrderedAddGroup.mk ⋯

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

Equations

• Additive.normedOrderedAddGroup = NormedOrderedAddGroup.mk ⋯

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

Equations

• Multiplicative.normedOrderedGroup = NormedOrderedGroup.mk ⋯

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

Equations

• Additive.normedLinearOrderedAddGroup = NormedLinearOrderedAddGroup.mk ⋯

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

Equations

• Multiplicative.normedlinearOrderedGroup = NormedLinearOrderedGroup.mk ⋯