# Documentation

Mathlib.Analysis.Normed.Order.Basic

# 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 , , :
Type u_2
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), = a +
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑()) 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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology :
• cobounded_sets : ().sets = {s_1 | C, ∀ (x : α), x s_1∀ (y : α), y s_1dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = 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.

Instances
class NormedOrderedGroup (α : Type u_2) extends , , :
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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), = a *
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑()) 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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology :
• cobounded_sets : ().sets = {s_1 | C, ∀ (x : α), x s_1∀ (y : α), y s_1dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = 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.

Instances
class NormedLinearOrderedAddGroup (α : Type u_2) extends , , :
Type u_2
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), = a +
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑()) 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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 :
• 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 =
• 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 : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology :
• cobounded_sets : ().sets = {s_1 | C, ∀ (x : α), x s_1∀ (y : α), y s_1dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = 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.

Instances
class NormedLinearOrderedGroup (α : Type u_2) extends , , :
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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), = a *
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑()) 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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 :
• 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 =
• 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 : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology :
• cobounded_sets : ().sets = {s_1 | C, ∀ (x : α), x s_1∀ (y : α), y s_1dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = 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.

Instances
class NormedLinearOrderedField (α : Type u_2) extends , , :
Type u_2
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) 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_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = x *
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul () a = a + Ring.zsmul () a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (↑()) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -↑(n + 1)
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 < a0 < b0 < a * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• 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 =
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α),
• zpow_succ' : ∀ (n : ) (a : α), =
• zpow_neg' : ∀ (n : ) (a : α), = (LinearOrderedField.zpow (↑()) a)⁻¹
• ratCast : α
• mul_inv_cancel : ∀ (a : α), a 0a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• ratCast_mk : ∀ (a : ) (b : ) (h1 : b 0) (h2 : ), ↑(Rat.mk' a b) = a * (b)⁻¹
• qsmul : αα
• qsmul_eq_mul' : ∀ (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 : α), = ENNReal.ofReal (dist x y)
• toUniformSpace :
• uniformity_dist : = ⨅ (ε : ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology :
• cobounded_sets : ().sets = {s_1 | C, ∀ (x : α), x s_1∀ (y : α), y s_1dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = 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.

Instances
noncomputable instance Real.normedLinearOrderedField :
theorem OrderDual.normedOrderedAddGroup.proof_1 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
a b∀ (c : αᵒᵈ), c + a c + b
theorem OrderDual.normedLinearOrderedAddGroup.proof_2 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
min a b = if a b then a else b
theorem OrderDual.normedLinearOrderedAddGroup.proof_3 {α : Type u_1} (a : αᵒᵈ) (b : αᵒᵈ) :
max a b = if a b then b else a