mathlib documentation

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.

References #

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

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
theorem solid {α : Type u_1} [normed_lattice_add_comm_group α] {a b : α} (h : |a| |b|) :
@[protected, instance]
def order_dual.normed_group {α : Type u_1} [normed_group α] :

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} [normed_lattice_add_comm_group α] (a b : α) (h : b -b a -a) :

Let α be a normed lattice ordered group and let a and b be elements of α. Then a⊓-a ≥ b⊓-b implies ∥a∥ ≤ ∥b∥.

theorem norm_abs_eq_norm {α : Type u_1} [normed_lattice_add_comm_group α] (a : α) :

Let α be a normed lattice ordered group, let a be an element of α and let |a| be the absolute value of a. Then ∥|a|∥ = ∥a∥.

@[protected, instance]

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

@[protected, instance]

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

Equations