Documentation

Mathlib.Algebra.Order.Group.Lattice

Lattice ordered groups #

Lattice ordered groups were introduced by [Birkhoff][birkhoff1942]. They form the algebraic underpinnings of vector lattices, Banach lattices, AL-space, AM-space etc.

A lattice ordered group is a type α satisfying:

This file establishes basic properties of lattice ordered groups. It is shown that when the group is commutative, the lattice is distributive. This also holds in the non-commutative case ([Birkhoff][birkhoff1942],[Fuchs][fuchs1963]) but we do not yet have the machinery to establish this in mathlib.

References #

Tags #

lattice, order, group

theorem add_sup {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c + a b = (c + a) (c + b)
theorem mul_sup {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c * (a b) = c * a c * b
theorem sup_add {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b + c = (a + c) (b + c)
theorem sup_mul {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) * c = a * c b * c
theorem add_inf {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c + a b = (c + a) (c + b)
theorem mul_inf {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c * (a b) = c * a c * b
theorem inf_add {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b + c = (a + c) (b + c)
theorem inf_mul {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) * c = a * c b * c
theorem sup_sub {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b - c = (a - c) (b - c)
theorem sup_div {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) / c = a / c b / c
theorem inf_sub {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
a b - c = (a - c) (b - c)
theorem inf_div {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
(a b) / c = a / c b / c
theorem neg_sup {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
-(a b) = -a -b
theorem inv_sup {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
theorem neg_inf {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
-(a b) = -a -b
theorem inv_inf {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
theorem sub_sup {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c - a b = (c - a) (c - b)
theorem div_sup {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c / (a b) = c / a c / b
theorem sub_inf {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c - a b = (c - a) (c - b)
theorem div_inf {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) (c : α) :
c / (a b) = c / a c / b
theorem nsmul_two_semiclosed {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} (ha : 0 2 a) :
0 a
theorem pow_two_semiclosed {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} (ha : 1 a ^ 2) :
1 a
theorem inf_add_sup {α : Type u_1} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
a b + a b = a + b
theorem inf_mul_sup {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
(a b) * (a b) = a * b
def AddCommGroup.toDistribLattice (α : Type u_3) [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :

Every lattice ordered commutative additive group is a distributive lattice

Equations
Instances For
    theorem AddCommGroup.toDistribLattice.proof_1 (α : Type u_1) [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (x : α) (y : α) (z : α) :
    (x y) (x z) x y z
    def CommGroup.toDistribLattice (α : Type u_3) [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :

    Every lattice ordered commutative group is a distributive lattice.

    Equations
    Instances For