Documentation

Mathlib.Algebra.Order.Group.PosPart

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

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⁻¹⁻

@[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 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_nsmul_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_nsmul_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|

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|

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