Order units

This file introduces the two standard notions of order unit in a vector lattice. A weak order unit is a non-negative element disjoint only from zero, while a strong order unit is a non-negative element which dominates every other element up to a positive scalar multiple. Every strong order unit is a weak order unit.

def WeakOrderUnit {X : Type u_1} [AddCommGroup X] [Lattice X] (e : X) : Prop

An element e of a vector lattice is a weak order unit if it is non-negative and the only element disjoint from e is 0.

Equations

• WeakOrderUnit e = (0 ≤ e ∧ ∀ (x : X), IsVLDisjoint x e → x = 0)

def StrongOrderUnit {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] (e : X) : Prop

An element e of a vector lattice is a strong order unit if it is non-negative and every element of X is dominated, in absolute value, by some non-negative real multiple of e.

Equations

• StrongOrderUnit e = (0 ≤ e ∧ ∀ (x : X), ∃ (c : ℝ), 0 ≤ c ∧ |x| ≤ c • e)

theorem WeakOrderUnit.of_strongOrderUnit {X : Type u_1} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {e : X} (he : StrongOrderUnit e) : WeakOrderUnit e

Every strong order unit is a weak order unit.