Documentation

Mathlib.Algebra.Order.LatticeGroup

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.

This file develops the basic theory.

Main statements #

pos_div_neg: Every element a of a lattice ordered group has a decomposition a⁺-a⁻ into the difference of the positive and negative component.
pos_inf_neg_eq_one: The positive and negative components are coprime.
abs_triangle: The absolute value operation satisfies the triangle inequality (stated for a commutative group).

It is shown that the inf and sup operations are related to the absolute value operation by a number of equations and inequalities.

Notations #

a⁺ = a ⊔ 0: The positive component of an element a of a lattice ordered group
a⁻ = (-a) ⊔ 0: The negative component of an element a of a lattice ordered group
|a| = a⊔(-a): The absolute value of an element a of a lattice ordered group

Implementation notes #

A lattice ordered group is a type α satisfying:

[Lattice α]
[CommGroup α]
[CovariantClass α α (*) (≤)]
[CovariantClass α α (swap (· * ·)) (· ≤ ·)]

The remainder of the 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 #

[Birkhoff, Lattice-ordered Groups][birkhoff1942]
[Bourbaki, Algebra II][bourbaki1981]
[Fuchs, Partially Ordered Algebraic Systems][fuchs1963]
[Zaanen, Lectures on "Riesz Spaces"][zaanen1966]
[Banasiak, Banach Lattices in Applications][banasiak]

Tags #

lattice, ordered, group

theorem add_sup {α : Type u} [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} [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} [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} [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} [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} [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} [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} [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_eq_neg_inf_neg {α : Type u} [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_eq_inv_inf_inv {α : Type u} [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 : α) :

(a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹

theorem neg_inf_eq_sup_neg {α : Type u} [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_eq_sup_inv {α : Type u} [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 : α) :

(a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹

instance LatticeOrderedGroup.hasZeroLatticeHasPosPart {α : Type u} [Lattice α] [AddGroup α] :

Let α be a lattice ordered commutative group with identity 0. For an element a of type α,the element a ⊔ 0 is said to be the positive component of a, denoted a⁺.

Equations

LatticeOrderedGroup.hasZeroLatticeHasPosPart = { pos := fun (a : α) => a ⊔ 0 }

instance LatticeOrderedGroup.hasOneLatticeHasPosPart {α : Type u} [Lattice α] [Group α] :

Let α be a lattice ordered commutative group with identity 1. For an element a of type α, the element a ⊔ 1 is said to be the positive component of a, denoted a⁺.

Equations

LatticeOrderedGroup.hasOneLatticeHasPosPart = { pos := fun (a : α) => a ⊔ 1 }

theorem LatticeOrderedGroup.pos_part_def {α : Type u} [Lattice α] [AddGroup α] (a : α) :

a⁺ = a ⊔ 0

theorem LatticeOrderedGroup.m_pos_part_def {α : Type u} [Lattice α] [Group α] (a : α) :

a⁺ = a ⊔ 1

instance LatticeOrderedGroup.hasZeroLatticeHasNegPart {α : Type u} [Lattice α] [AddGroup α] :

Let α be a lattice ordered commutative group with identity 0. For an element a of type α, the element (-a) ⊔ 0 is said to be the negative component of a, denoted a⁻.

Equations

LatticeOrderedGroup.hasZeroLatticeHasNegPart = { neg := fun (a : α) => -a ⊔ 0 }

instance LatticeOrderedGroup.hasOneLatticeHasNegPart {α : Type u} [Lattice α] [Group α] :

Let α be a lattice ordered commutative group with identity 1. For an element a of type α, the element (-a) ⊔ 1 is said to be the negative component of a, denoted a⁻.

Equations

LatticeOrderedGroup.hasOneLatticeHasNegPart = { neg := fun (a : α) => a⁻¹ ⊔ 1 }

theorem LatticeOrderedGroup.neg_part_def {α : Type u} [Lattice α] [AddGroup α] (a : α) :

a⁻ = -a ⊔ 0

theorem LatticeOrderedGroup.m_neg_part_def {α : Type u} [Lattice α] [Group α] (a : α) :

a⁻ = a⁻¹ ⊔ 1

@[simp]

theorem LatticeOrderedGroup.pos_zero {α : Type u} [Lattice α] [AddGroup α] :

0⁺ = 0

@[simp]

theorem LatticeOrderedGroup.pos_one {α : Type u} [Lattice α] [Group α] :

1⁺ = 1

@[simp]

theorem LatticeOrderedGroup.neg_zero {α : Type u} [Lattice α] [AddGroup α] :

0⁻ = 0

@[simp]

theorem LatticeOrderedGroup.neg_one {α : Type u} [Lattice α] [Group α] :

1⁻ = 1

theorem LatticeOrderedGroup.neg_eq_neg_inf_zero {α : Type u} [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 : α) :

a⁻ = -(a ⊓ 0)

theorem LatticeOrderedGroup.neg_eq_inv_inf_one {α : Type u} [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 : α) :

a⁻ = (a ⊓ 1)⁻¹

theorem LatticeOrderedGroup.le_abs {α : Type u} [Lattice α] [AddGroup α] (a : α) :

a ≤ |a|

theorem LatticeOrderedGroup.le_mabs {α : Type u} [Lattice α] [Group α] (a : α) :

a ≤ |a|

theorem LatticeOrderedGroup.neg_le_abs {α : Type u} [Lattice α] [AddGroup α] (a : α) :

-a ≤ |a|

theorem LatticeOrderedGroup.inv_le_abs {α : Type u} [Lattice α] [Group α] (a : α) :

@[simp]

theorem LatticeOrderedGroup.abs_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

|(-a)| = |a|

@[simp]

theorem LatticeOrderedGroup.abs_inv {α : Type u} [Lattice α] [Group α] (a : α) :

|a⁻¹| = |a|

theorem LatticeOrderedGroup.pos_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.one_le_pos {α : Type u} [Lattice α] [Group α] (a : α) :

theorem LatticeOrderedGroup.neg_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.one_le_neg {α : Type u} [Lattice α] [Group α] (a : α) :

theorem LatticeOrderedGroup.pos_nonpos_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} :

a⁺ ≤ 0 ↔ a ≤ 0

theorem LatticeOrderedGroup.pos_le_one_iff {α : Type u} [Lattice α] [Group α] {a : α} :

a⁺ ≤ 1 ↔ a ≤ 1

theorem LatticeOrderedGroup.neg_nonpos_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} :

a⁻ ≤ 0 ↔ -a ≤ 0

theorem LatticeOrderedGroup.neg_le_one_iff {α : Type u} [Lattice α] [Group α] {a : α} :

a⁻ ≤ 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedGroup.pos_eq_zero_iff {α : Type u} [Lattice α] [AddGroup α] {a : α} :

a⁺ = 0 ↔ a ≤ 0

theorem LatticeOrderedGroup.pos_eq_one_iff {α : Type u} [Lattice α] [Group α] {a : α} :

a⁺ = 1 ↔ a ≤ 1

theorem LatticeOrderedGroup.neg_eq_zero_iff' {α : Type u} [Lattice α] [AddGroup α] {a : α} :

a⁻ = 0 ↔ -a ≤ 0

theorem LatticeOrderedGroup.neg_eq_one_iff' {α : Type u} [Lattice α] [Group α] {a : α} :

a⁻ = 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedGroup.neg_eq_zero_iff {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α HAdd.hAdd LE.le] {a : α} :

a⁻ = 0 ↔ 0 ≤ a

theorem LatticeOrderedGroup.neg_eq_one_iff {α : Type u} [Lattice α] [Group α] [CovariantClass α α HMul.hMul LE.le] {a : α} :

a⁻ = 1 ↔ 1 ≤ a

theorem LatticeOrderedGroup.le_pos {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.m_le_pos {α : Type u} [Lattice α] [Group α] (a : α) :

theorem LatticeOrderedGroup.neg_le_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.inv_le_neg {α : Type u} [Lattice α] [Group α] (a : α) :

a⁻¹ ≤ a⁻

theorem LatticeOrderedGroup.neg_eq_pos_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.neg_eq_pos_inv {α : Type u} [Lattice α] [Group α] (a : α) :

a⁻ = a⁻¹⁺

theorem LatticeOrderedGroup.pos_eq_neg_neg {α : Type u} [Lattice α] [AddGroup α] (a : α) :

theorem LatticeOrderedGroup.pos_eq_neg_inv {α : Type u} [Lattice α] [Group α] (a : α) :

a⁺ = a⁻¹⁻

theorem LatticeOrderedGroup.add_inf_eq_add_inf_add {α : Type u} [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 LatticeOrderedGroup.mul_inf_eq_mul_inf_mul {α : Type u} [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

@[simp]

theorem LatticeOrderedGroup.pos_sub_neg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) :

a⁺ - a⁻ = a

@[simp]

theorem LatticeOrderedGroup.pos_div_neg {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) :

a⁺ / a⁻ = a

theorem LatticeOrderedGroup.pos_of_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : 0 ≤ a) :

a⁺ = a

If a is positive, then it is equal to its positive component a⁺.

theorem LatticeOrderedGroup.pos_of_one_le {α : Type u} [Lattice α] [Group α] (a : α) (h : 1 ≤ a) :

a⁺ = a

If a is positive, then it is equal to its positive component a⁺.

theorem LatticeOrderedGroup.pos_of_nonpos {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : a ≤ 0) :

a⁺ = 0

theorem LatticeOrderedGroup.pos_of_le_one {α : Type u} [Lattice α] [Group α] (a : α) (h : a ≤ 1) :

a⁺ = 1

theorem LatticeOrderedGroup.neg_of_inv_nonneg {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : 0 ≤ -a) :

theorem LatticeOrderedGroup.neg_of_one_le_inv {α : Type u} [Lattice α] [Group α] (a : α) (h : 1 ≤ a⁻¹) :

theorem LatticeOrderedGroup.neg_of_neg_nonpos {α : Type u} [Lattice α] [AddGroup α] (a : α) (h : -a ≤ 0) :

a⁻ = 0

theorem LatticeOrderedGroup.neg_of_inv_le_one {α : Type u} [Lattice α] [Group α] (a : α) (h : a⁻¹ ≤ 1) :

a⁻ = 1

theorem LatticeOrderedGroup.neg_of_nonpos {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : a ≤ 0) :

theorem LatticeOrderedGroup.neg_of_le_one {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : a ≤ 1) :

theorem LatticeOrderedGroup.pos_eq_self_of_pos_pos {α : Type u_1} [LinearOrder α] [AddCommGroup α] {x : α} (hx : 0 < x⁺) :

x⁺ = x

theorem LatticeOrderedGroup.pos_eq_self_of_one_lt_pos {α : Type u_1} [LinearOrder α] [CommGroup α] {x : α} (hx : 1 < x⁺) :

x⁺ = x

theorem LatticeOrderedGroup.neg_of_nonneg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 0 ≤ a) :

a⁻ = 0

theorem LatticeOrderedGroup.neg_of_one_le {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 1 ≤ a) :

a⁻ = 1

theorem LatticeOrderedGroup.abs_of_nonneg {α : Type u} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 0 ≤ a) :

|a| = a

theorem LatticeOrderedGroup.mabs_of_one_le {α : Type u} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (h : 1 ≤ a) :

|a| = a

theorem LatticeOrderedGroup.abs_sub_comm {α : Type u} [Lattice α] [AddGroup α] (a : α) (b : α) :

|a - b| = |b - a|

theorem LatticeOrderedGroup.abs_div_comm {α : Type u} [Lattice α] [Group α] (a : α) (b : α) :

|a / b| = |b / a|

theorem LatticeOrderedGroup.nsmul_two_semiclosed {α : Type u} [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 : α) :

0 ≤ 2 • a → 0 ≤ a

theorem LatticeOrderedGroup.pow_two_semiclosed {α : Type u} [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 : α) :

1 ≤ a ^ 2 → 1 ≤ a

theorem LatticeOrderedGroup.abs_nonneg {α : Type u} [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 : α) :

0 ≤ |a|

theorem LatticeOrderedGroup.one_le_abs {α : Type u} [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 : α) :

1 ≤ |a|

theorem LatticeOrderedGroup.pos_add_neg {α : Type u} [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 : α) :

|a| = a⁺ + a⁻

theorem LatticeOrderedGroup.pos_mul_neg {α : Type u} [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 : α) :

|a| = a⁺ * a⁻

theorem LatticeOrderedGroup.pos_abs {α : Type u} [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 : α) :

|a|⁺ = |a|

theorem LatticeOrderedGroup.m_pos_abs {α : Type u} [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 : α) :

|a|⁺ = |a|

theorem LatticeOrderedGroup.neg_abs {α : Type u} [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 : α) :

|a|⁻ = 0

theorem LatticeOrderedGroup.m_neg_abs {α : Type u} [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 : α) :

|a|⁻ = 1

theorem LatticeOrderedGroup.sup_sub_inf_eq_abs_sub {α : Type u} [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 = |b - a|

theorem LatticeOrderedGroup.sup_div_inf_eq_abs_div {α : Type u} [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 : α) :

(a ⊔ b) / (a ⊓ b) = |b / a|

@[simp]

theorem LatticeOrderedGroup.abs_abs {α : Type u} [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 : α) :

|(|a|)| = |a|

The unary operation of taking the absolute value is idempotent.

@[simp]

theorem LatticeOrderedGroup.mabs_mabs {α : Type u} [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 : α) :

|(|a|)| = |a|

The unary operation of taking the absolute value is idempotent.

theorem LatticeOrderedGroup.pos_inf_neg_eq_zero {α : Type u} [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 : α) :

a⁺ ⊓ a⁻ = 0

theorem LatticeOrderedGroup.pos_inf_neg_eq_one {α : Type u} [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 : α) :

a⁺ ⊓ a⁻ = 1

theorem inf_add_sup {α : Type u} [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} [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

theorem LatticeOrderedCommGroup.sup_eq_add_pos_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ⊔ b = b + (a - b)⁺

theorem LatticeOrderedCommGroup.sup_eq_mul_pos_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ⊔ b = b * (a / b)⁺

theorem LatticeOrderedCommGroup.inf_eq_sub_pos_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ⊓ b = a - (a - b)⁺

theorem LatticeOrderedCommGroup.inf_eq_div_pos_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ⊓ b = a / (a / b)⁺

theorem LatticeOrderedCommGroup.le_iff_pos_le_neg_ge {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

theorem LatticeOrderedCommGroup.m_le_iff_pos_le_neg_ge {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

a ≤ b ↔ a⁺ ≤ b⁺ ∧ b⁻ ≤ a⁻

theorem LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

2 • (a ⊔ b) = a + b + |b - a|

theorem LatticeOrderedCommGroup.sup_sq_eq_mul_mul_abs_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

(a ⊔ b) ^ 2 = a * b * |b / a|

theorem LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

2 • (a ⊓ b) = a + b - |b - a|

theorem LatticeOrderedCommGroup.inf_sq_eq_mul_div_abs_div {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

(a ⊓ b) ^ 2 = a * b / |b / a|

def LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice (α : Type u) [s : Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] :

DistribLattice α

Every lattice ordered commutative additive group is a distributive lattice

Equations

LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice α = DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

Instances For

theorem LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice.proof_1 (α : Type u_1) [s : 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 LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice (α : Type u) [s : Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] :

DistribLattice α

Every lattice ordered commutative group is a distributive lattice

Equations

LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice α = DistribLattice.mk (_ : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

Instances For

theorem LatticeOrderedCommGroup.abs_sub_sup_add_abs_sub_inf {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|a ⊔ c - b ⊔ c| + |a ⊓ c - b ⊓ c| = |a - b|

theorem LatticeOrderedCommGroup.abs_div_sup_mul_abs_div_inf {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|(a ⊔ c) / (b ⊔ c)| * |(a ⊓ c) / (b ⊓ c)| = |a / b|

theorem LatticeOrderedCommGroup.abs_sup_sub_sup_le_abs {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|a ⊔ c - b ⊔ c| ≤ |a - b|

theorem LatticeOrderedCommGroup.mabs_sup_div_sup_le_mabs {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|(a ⊔ c) / (b ⊔ c)| ≤ |a / b|

theorem LatticeOrderedCommGroup.abs_inf_sub_inf_le_abs {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|a ⊓ c - b ⊓ c| ≤ |a - b|

theorem LatticeOrderedCommGroup.mabs_inf_div_inf_le_mabs {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|(a ⊓ c) / (b ⊓ c)| ≤ |a / b|

theorem LatticeOrderedCommGroup.Birkhoff_inequalities {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|a ⊔ c - b ⊔ c| ⊔ |a ⊓ c - b ⊓ c| ≤ |a - b|

theorem LatticeOrderedCommGroup.m_Birkhoff_inequalities {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) :

|(a ⊔ c) / (b ⊔ c)| ⊔ |(a ⊓ c) / (b ⊓ c)| ≤ |a / b|

theorem LatticeOrderedCommGroup.abs_add_le {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

|a + b| ≤ |a| + |b|

The absolute value satisfies the triangle inequality.

theorem LatticeOrderedCommGroup.mabs_mul_le {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

|a * b| ≤ |a| * |b|

The absolute value satisfies the triangle inequality.

theorem LatticeOrderedCommGroup.abs_abs_sub_abs_le {α : Type u} [Lattice α] [AddCommGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

||a| - |b|| ≤ |a - b|

theorem LatticeOrderedCommGroup.abs_abs_div_abs_le {α : Type u} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) :

||a| / |b|| ≤ |a / b|

theorem inf_eq_half_smul_add_sub_abs_sub (α : Type u) {β : Type v} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] (x : β) (y : β) :

x ⊓ y = ⅟2 • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub (α : Type u) {β : Type v} [Semiring α] [Invertible 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] (x : β) (y : β) :

x ⊔ y = ⅟2 • (x + y + |y - x|)

theorem inf_eq_half_smul_add_sub_abs_sub' (α : Type u) {β : Type v} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] (x : β) (y : β) :

x ⊓ y = 2⁻¹ • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub' (α : Type u) {β : Type v} [DivisionSemiring α] [NeZero 2] [Lattice β] [AddCommGroup β] [Module α β] [CovariantClass β β (fun (x x_1 : β) => x + x_1) fun (x x_1 : β) => x ≤ x_1] (x : β) (y : β) :

x ⊔ y = 2⁻¹ • (x + y + |y - x|)

def LatticeOrderedAddCommGroup.IsSolid {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) :

A subset s ⊆ β, with β an AddCommGroup with a Lattice structure, is solid if for all x ∈ s and all y ∈ β such that |y| ≤ |x|, then y ∈ s.

Equations

LatticeOrderedAddCommGroup.IsSolid s = ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, |y| ≤ |x| → y ∈ s

Instances For

def LatticeOrderedAddCommGroup.solidClosure {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) :

Set β

The solid closure of a subset s is the smallest superset of s that is solid.

Equations

LatticeOrderedAddCommGroup.solidClosure s = {y : β | ∃ x ∈ s, |y| ≤ |x|}

Instances For

theorem LatticeOrderedAddCommGroup.isSolid_solidClosure {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) :

LatticeOrderedAddCommGroup.IsSolid (LatticeOrderedAddCommGroup.solidClosure s)

theorem LatticeOrderedAddCommGroup.solidClosure_min {β : Type v} [Lattice β] [AddCommGroup β] (s : Set β) (t : Set β) (h1 : s ⊆ t) (h2 : LatticeOrderedAddCommGroup.IsSolid t) :

LatticeOrderedAddCommGroup.solidClosure s ⊆ t