# mathlibdocumentation

analysis.normed_space.lattice_ordered_group

# Normed lattice ordered groups #

Motivated by the theory of Banach Lattices, we then define normed_lattice_add_comm_group 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 orderd groups #

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

@[class]
structure normed_lattice_add_comm_group (α : Type u_1) :
Type u_1
• to_lattice :
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• solid : ∀ (a b : α), |a| |b|a b

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.

Instances of this typeclass
Instances of other typeclasses for normed_lattice_add_comm_group
theorem solid {α : Type u_1} {a b : α} (h : |a| |b|) :
@[protected, instance]
Equations
@[protected, instance]

A normed lattice ordered group is an ordered additive commutative group

Equations
@[protected, instance]
def order_dual.normed_add_comm_group {α : Type u_1}  :

Let α be a normed group with a partial order. Then the order dual is also a normed group.

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

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

Equations
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 : α) :
@[protected, instance]

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

@[protected, instance]
@[protected, instance]

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 : α) :
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 lipschitz_with_sup_right {α : Type u_1} (z : α) :
(λ (x : α), x z)
theorem lipschitz_with_pos {α : Type u_1}  :
theorem continuous_pos {α : Type u_1}  :
theorem continuous_neg' {α : Type u_1}  :
theorem is_closed_nonneg {E : Type u_1}  :
is_closed {x : E | 0 x}
theorem is_closed_le_of_is_closed_nonneg {G : Type u_1} (h : is_closed {x : G | 0 x}) :
is_closed {p : G × G | p.fst p.snd}
@[protected, instance]