# Normed lattice ordered groups #

Motivated by the theory of Banach Lattices, we then define NormedLatticeAddCommGroup as a lattice with a covariant normed group addition satisfying the solid axiom.

## Main statements #

We show that a normed lattice ordered group is a topological lattice with respect to the norm topology.

## Tags #

normed, lattice, ordered, group

### Normed lattice ordered groups #

Motivated by the theory of Banach Lattices, this section introduces normed lattice ordered groups.

class HasSolidNorm (α : Type u_1) [] :

Let α be an AddCommGroup with a Lattice structure. A norm on α is solid if, for a and b in α, with absolute values |a| and |b| respectively, |a| ≤ |b| implies ‖a‖ ≤ ‖b‖.

Instances
theorem HasSolidNorm.solid {α : Type u_1} [] [self : ] ⦃x : α ⦃y : α :
|x| |y|x y
theorem norm_le_norm_of_abs_le_abs {α : Type u_1} [] [] {a : α} {b : α} (h : |a| |b|) :
theorem LatticeOrderedAddCommGroup.isSolid_ball {α : Type u_1} [] [] (r : ) :

If α has a solid norm, then the balls centered at the origin of α are solid sets.

Equations
Equations
class NormedLatticeAddCommGroup (α : Type u_1) extends , , :
Type u_1

Let α be a normed commutative group equipped with a partial order covariant with addition, with respect which α forms a lattice. Suppose that α is solid, that is to say, for a and b in α, with absolute values |a| and |b| respectively, |a| ≤ |b| implies ‖a‖ ≤ ‖b‖. Then α is said to be a normed lattice ordered group.

• norm : α
• 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 : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• 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.1 p.2 < ε}
• toBornology :
• cobounded_sets : .sets = {s : Set α | ∃ (C : ), xs, ys, dist x y C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0x = y
• dist_eq : ∀ (x y : α), dist x y = x - y
• sup : ααα
• 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
• le_sup_left : ∀ (a b : α), a a b
• le_sup_right : ∀ (a b : α), b a b
• sup_le : ∀ (a b c : α), a cb ca b c
• inf : ααα
• inf_le_left : ∀ (a b : α), a b a
• inf_le_right : ∀ (a b : α), a b b
• le_inf : ∀ (a b c : α), a ba ca b c
• solid : ∀ ⦃x y : α⦄, |x| |y|x y
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
Instances
a b∀ (c : α), c + a c + b
@[instance 100]

A normed lattice ordered group is an ordered additive commutative group

Equations
theorem dual_solid {α : Type u_1} (a : α) (b : α) (h : b -b a -a) :
@[instance 100]

Let α be a normed lattice ordered group, then the order dual is also a normed lattice ordered group.

Equations
• One or more equations did not get rendered due to their size.
theorem norm_abs_eq_norm {α : Type u_1} (a : α) :
theorem norm_inf_sub_inf_le_add_norm {α : Type u_1} (a : α) (b : α) (c : α) (d : α) :
a b - c d a - c + b - d
theorem norm_sup_sub_sup_le_add_norm {α : Type u_1} (a : α) (b : α) (c : α) (d : α) :
a b - c d a - c + b - d
theorem norm_inf_le_add {α : Type u_1} (x : α) (y : α) :
theorem norm_sup_le_add {α : Type u_1} (x : α) (y : α) :
@[instance 100]

Let α be a normed lattice ordered group. Then the infimum is jointly continuous.

Equations
• =
@[instance 100]
Equations
• =
@[instance 100]

Let α be a normed lattice ordered group. Then α is a topological lattice in the norm topology.

Equations
• =
theorem norm_abs_sub_abs {α : Type u_1} (a : α) (b : α) :
|a| - |b| a - b
theorem norm_sup_sub_sup_le_norm {α : Type u_1} (x : α) (y : α) (z : α) :
x z - y z x - y
theorem norm_inf_sub_inf_le_norm {α : Type u_1} (x : α) (y : α) (z : α) :
x z - y z x - y
theorem lipschitzWith_sup_right {α : Type u_1} (z : α) :
LipschitzWith 1 fun (x : α) => x z
theorem lipschitzWith_posPart {α : Type u_1} :
LipschitzWith 1 posPart
theorem lipschitzWith_negPart {α : Type u_1} :
LipschitzWith 1 negPart
theorem continuous_posPart {α : Type u_1} :
Continuous posPart
theorem continuous_negPart {α : Type u_1} :
Continuous negPart
theorem isClosed_nonneg {α : Type u_1} :
IsClosed {x : α | 0 x}
theorem isClosed_le_of_isClosed_nonneg {G : Type u_2} [] [] (h : IsClosed {x : G | 0 x}) :
IsClosed {p : G × G | p.1 p.2}
@[instance 100]
Equations
• =