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, concentrating on the commutative case.

Main statements #

pos_div_neg: Every element a of a lattice ordered commutative 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.

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 commutative group
a⁻ = (-a) ⊔ 0: The negative component of an element a of a lattice ordered commutative group
|a| = a⊔(-a): The absolute value of an element a of a lattice ordered commutative group

Implementation notes #

A lattice ordered commutative group is a type α satisfying:

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

The remainder of the file establishes basic properties of lattice ordered commutative groups. A number of these results also hold in the non-commutative case ([Birkhoff][birkhoff1942], [Fuchs][fuchs1963]) but we have not developed that here, since we are primarily interested in vector lattices.

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

def LinearOrderedAddCommGroup.to_covariantClass.proof_1 (α : Type u_1) [inst : LinearOrderedAddCommGroup α] :

CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

(_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1) = (_ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1)

instance LinearOrderedAddCommGroup.to_covariantClass (α : Type u) [inst : LinearOrderedAddCommGroup α] :

CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

Equations

LinearOrderedAddCommGroup.to_covariantClass = LinearOrderedAddCommGroup.to_covariantClass.proof_1

instance LinearOrderedCommGroup.to_covariantClass (α : Type u) [inst : LinearOrderedCommGroup α] :

CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

Equations

LinearOrderedCommGroup.to_covariantClass = LinearOrderedCommGroup.to_covariantClass.proof_1

theorem add_sup {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : 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 add_inf {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : 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 neg_sup_eq_neg_inf_neg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : CovariantClass α α (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} [inst : Lattice α] [inst : CommGroup α] [inst : CovariantClass α α (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} [inst : Lattice α] [inst : AddCommGroup α] [inst : CovariantClass α α (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} [inst : Lattice α] [inst : CommGroup α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) :

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

theorem inf_add_sup {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) :

(a ⊓ b) * (a ⊔ b) = a * b

instance LatticeOrderedCommGroup.hasZeroLatticeHasPosPart {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] :

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

LatticeOrderedCommGroup.hasZeroLatticeHasPosPart = { pos := fun a => a ⊔ 0 }

instance LatticeOrderedCommGroup.hasOneLatticeHasPosPart {α : Type u} [inst : Lattice α] [inst : CommGroup α] :

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

LatticeOrderedCommGroup.hasOneLatticeHasPosPart = { pos := fun a => a ⊔ 1 }

theorem LatticeOrderedCommGroup.pos_part_def {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

a⁺ = a ⊔ 0

theorem LatticeOrderedCommGroup.m_pos_part_def {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁺ = a ⊔ 1

instance LatticeOrderedCommGroup.hasZeroLatticeHasNegPart {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] :

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

LatticeOrderedCommGroup.hasZeroLatticeHasNegPart = { neg := fun a => -a ⊔ 0 }

instance LatticeOrderedCommGroup.hasOneLatticeHasNegPart {α : Type u} [inst : Lattice α] [inst : CommGroup α] :

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

LatticeOrderedCommGroup.hasOneLatticeHasNegPart = { neg := fun a => a⁻¹ ⊔ 1 }

theorem LatticeOrderedCommGroup.neg_part_def {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

a⁻ = -a ⊔ 0

theorem LatticeOrderedCommGroup.m_neg_part_def {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁻ = a⁻¹ ⊔ 1

@[simp]

theorem LatticeOrderedCommGroup.pos_zero {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] :

0⁺ = 0

@[simp]

theorem LatticeOrderedCommGroup.pos_one {α : Type u} [inst : Lattice α] [inst : CommGroup α] :

1⁺ = 1

@[simp]

theorem LatticeOrderedCommGroup.neg_zero {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] :

0⁻ = 0

@[simp]

theorem LatticeOrderedCommGroup.neg_one {α : Type u} [inst : Lattice α] [inst : CommGroup α] :

1⁻ = 1

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

a⁻ = -(a ⊓ 0)

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

a⁻ = (a ⊓ 1)⁻¹

theorem LatticeOrderedCommGroup.le_abs {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.le_mabs {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.neg_le_abs {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.inv_le_abs {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁻¹ ≤ abs a

theorem LatticeOrderedCommGroup.pos_nonneg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.one_le_pos {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.neg_nonneg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.one_le_neg {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.pos_nonpos_iff {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] {a : α} :

a⁺ ≤ 0 ↔ a ≤ 0

theorem LatticeOrderedCommGroup.pos_le_one_iff {α : Type u} [inst : Lattice α] [inst : CommGroup α] {a : α} :

a⁺ ≤ 1 ↔ a ≤ 1

theorem LatticeOrderedCommGroup.neg_nonpos_iff {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] {a : α} :

a⁻ ≤ 0 ↔ -a ≤ 0

theorem LatticeOrderedCommGroup.neg_le_one_iff {α : Type u} [inst : Lattice α] [inst : CommGroup α] {a : α} :

a⁻ ≤ 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedCommGroup.pos_eq_zero_iff {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] {a : α} :

a⁺ = 0 ↔ a ≤ 0

theorem LatticeOrderedCommGroup.pos_eq_one_iff {α : Type u} [inst : Lattice α] [inst : CommGroup α] {a : α} :

a⁺ = 1 ↔ a ≤ 1

theorem LatticeOrderedCommGroup.neg_eq_zero_iff' {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] {a : α} :

a⁻ = 0 ↔ -a ≤ 0

theorem LatticeOrderedCommGroup.neg_eq_one_iff' {α : Type u} [inst : Lattice α] [inst : CommGroup α] {a : α} :

a⁻ = 1 ↔ a⁻¹ ≤ 1

theorem LatticeOrderedCommGroup.neg_eq_zero_iff {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : CovariantClass α α Add.add LE.le] {a : α} :

a⁻ = 0 ↔ 0 ≤ a

theorem LatticeOrderedCommGroup.neg_eq_one_iff {α : Type u} [inst : Lattice α] [inst : CommGroup α] [inst : CovariantClass α α Mul.mul LE.le] {a : α} :

a⁻ = 1 ↔ 1 ≤ a

theorem LatticeOrderedCommGroup.le_pos {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.m_le_pos {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.neg_le_neg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.inv_le_neg {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁻¹ ≤ a⁻

theorem LatticeOrderedCommGroup.neg_eq_pos_neg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.neg_eq_pos_inv {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁻ = a⁻¹⁺

theorem LatticeOrderedCommGroup.pos_eq_neg_neg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) :

theorem LatticeOrderedCommGroup.pos_eq_neg_inv {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) :

a⁺ = a⁻¹⁻

theorem LatticeOrderedCommGroup.add_inf_eq_add_inf_add {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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 LatticeOrderedCommGroup.mul_inf_eq_mul_inf_mul {α : Type u} [inst : Lattice α] [inst : CommGroup α] [inst : 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 LatticeOrderedCommGroup.pos_sub_neg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

a⁺ - a⁻ = a

@[simp]

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

a⁺ / a⁻ = a

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

a⁺ ⊓ a⁻ = 0

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

a⁺ ⊓ a⁻ = 1

theorem LatticeOrderedCommGroup.sup_eq_add_pos_sub {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : 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} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : 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} [inst : Lattice α] [inst : AddCommGroup α] [inst : 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} [inst : Lattice α] [inst : CommGroup α] [inst : 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.neg_abs {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) :

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

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

abs a⁺ = abs a

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

abs a⁺ = abs a

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

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

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

abs a = a⁺ + a⁻

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

abs a = a⁺ * a⁻

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

a ⊔ b - a ⊓ b = abs (b - a)

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

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

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

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

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

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

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

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

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

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

def LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice (α : Type u) [s : Lattice α] [inst : AddCommGroup α] [inst : 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)

def LatticeOrderedCommGroup.latticeOrderedAddCommGroupToDistribLattice.proof_1 (α : Type u_1) [s : Lattice α] [inst : AddCommGroup α] [inst : 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

Equations

(_ : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z) = (_ : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

def LatticeOrderedCommGroup.latticeOrderedCommGroupToDistribLattice (α : Type u) [s : Lattice α] [inst : CommGroup α] [inst : 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)

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

abs (a ⊔ c - b ⊔ c) + abs (a ⊓ c - b ⊓ c) = abs (a - b)

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

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

theorem LatticeOrderedCommGroup.pos_of_nonneg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) (h : 0 ≤ a) :

a⁺ = a

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

theorem LatticeOrderedCommGroup.pos_of_one_le {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) (h : 1 ≤ a) :

a⁺ = a

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

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

x⁺ = x

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

x⁺ = x

theorem LatticeOrderedCommGroup.pos_of_nonpos {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) (h : a ≤ 0) :

a⁺ = 0

theorem LatticeOrderedCommGroup.pos_of_le_one {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) (h : a ≤ 1) :

a⁺ = 1

theorem LatticeOrderedCommGroup.neg_of_inv_nonneg {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) (h : 0 ≤ -a) :

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

theorem LatticeOrderedCommGroup.neg_of_neg_nonpos {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) (h : -a ≤ 0) :

a⁻ = 0

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

a⁻ = 1

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

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

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

a⁻ = 0

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

a⁻ = 1

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

abs a = a

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

abs a = a

@[simp]

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

abs (abs a) = abs a

The unary operation of taking the absolute value is idempotent.

@[simp]

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

abs (abs a) = abs a

The unary operation of taking the absolute value is idempotent.

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

abs (a ⊔ c - b ⊔ c) ≤ abs (a - b)

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

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

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

abs (a ⊓ c - b ⊓ c) ≤ abs (a - b)

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

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

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

abs (a ⊔ c - b ⊔ c) ⊔ abs (a ⊓ c - b ⊓ c) ≤ abs (a - b)

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

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

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

abs (a + b) ≤ abs a + abs b

The absolute value satisfies the triangle inequality.

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

abs (a * b) ≤ abs a * abs b

The absolute value satisfies the triangle inequality.

theorem LatticeOrderedCommGroup.abs_neg_comm {α : Type u} [inst : Lattice α] [inst : AddCommGroup α] (a : α) (b : α) :

abs (a - b) = abs (b - a)

theorem LatticeOrderedCommGroup.abs_inv_comm {α : Type u} [inst : Lattice α] [inst : CommGroup α] (a : α) (b : α) :

abs (a / b) = abs (b / a)

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

abs (abs a - abs b) ≤ abs (a - b)

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

abs (abs a / abs b) ≤ abs (a / b)