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.
- to_normed_add_comm_group : normed_add_comm_group α
- to_lattice : 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
- normed_lattice_add_comm_group.has_sizeof_inst
Equations
- real.normed_lattice_add_comm_group = {to_normed_add_comm_group := real.normed_add_comm_group, to_lattice := real.lattice, add_le_add_left := real.normed_lattice_add_comm_group._proof_1, solid := real.normed_lattice_add_comm_group._proof_2}
A normed lattice ordered group is an ordered additive commutative group
Equations
- normed_lattice_add_comm_group_to_ordered_add_comm_group = {add := add_comm_group.add normed_add_comm_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero normed_add_comm_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul normed_add_comm_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg normed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub normed_add_comm_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul normed_add_comm_group.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, le := lattice.le normed_lattice_add_comm_group.to_lattice, lt := lattice.lt normed_lattice_add_comm_group.to_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _}
Let α
be a normed group with a partial order. Then the order dual is also a normed group.
Equations
Let α
be a normed lattice ordered group, then the order dual is also a
normed lattice ordered group.
Let α
be a normed lattice ordered group. Then the infimum is jointly continuous.
Let α
be a normed lattice ordered group. Then α
is a topological lattice in the norm topology.