# Absolute values in ordered groups #

The absolute value of an element in a group which is also a lattice is its supremum with its negation. This generalizes the usual absolute value on real numbers (|x| = max x (-x)).

## Notations #

• |a|: The absolute value of an element a of an additive lattice ordered group
• |a|ₘ: The absolute value of an element a of a multiplicative lattice ordered group
def abs {α : Type u_1} [] [] (a : α) :
α

abs a is the absolute value of a

Equations
Instances For
def mabs {α : Type u_1} [] [] (a : α) :
α

mabs a is the absolute value of a.

Equations
Instances For

mabs a is the absolute value of a.

Equations
• One or more equations did not get rendered due to their size.
Instances For

abs a is the absolute value of a

Equations
• One or more equations did not get rendered due to their size.
Instances For

Unexpander for the notation |a|ₘ for mabs a. Tries to add discretionary parentheses in unparseable cases.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Unexpander for the notation |a| for abs a. Tries to add discretionary parentheses in unparseable cases.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem abs_le' {α : Type u_1} [] [] {a : α} {b : α} :
|a| b a b -a b
theorem mabs_le' {α : Type u_1} [] [] {a : α} {b : α} :
mabs a b a b a⁻¹ b
theorem le_abs_self {α : Type u_1} [] [] (a : α) :
a |a|
theorem le_mabs_self {α : Type u_1} [] [] (a : α) :
a mabs a
theorem neg_le_abs {α : Type u_1} [] [] (a : α) :
-a |a|
theorem inv_le_mabs {α : Type u_1} [] [] (a : α) :
theorem abs_le_abs {α : Type u_1} [] [] {a : α} {b : α} (h₀ : a b) (h₁ : -a b) :
|a| |b|
theorem mabs_le_mabs {α : Type u_1} [] [] {a : α} {b : α} (h₀ : a b) (h₁ : a⁻¹ b) :
@[simp]
theorem abs_neg {α : Type u_1} [] [] (a : α) :
|(-a)| = |a|
@[simp]
theorem mabs_inv {α : Type u_1} [] [] (a : α) :
= mabs a
theorem abs_sub_comm {α : Type u_1} [] [] (a : α) (b : α) :
|a - b| = |b - a|
theorem mabs_div_comm {α : Type u_1} [] [] (a : α) (b : α) :
mabs (a / b) = mabs (b / a)
theorem abs_of_nonneg {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : 0 a) :
|a| = a
theorem mabs_of_one_le {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : 1 a) :
mabs a = a
theorem abs_of_pos {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : 0 < a) :
|a| = a
theorem mabs_of_one_lt {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : 1 < a) :
mabs a = a
theorem abs_of_nonpos {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : a 0) :
|a| = -a
theorem mabs_of_le_one {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : a 1) :
theorem abs_of_neg {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : a < 0) :
|a| = -a
theorem mabs_of_lt_one {α : Type u_1} [] [] {a : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : a < 1) :
theorem abs_le_abs_of_nonneg {α : Type u_1} [] [] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (ha : 0 a) (hab : a b) :
|a| |b|
theorem mabs_le_mabs_of_one_le {α : Type u_1} [] [] {a : α} {b : α} [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (ha : 1 a) (hab : a b) :
@[simp]
theorem abs_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
|0| = 0
@[simp]
theorem mabs_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
mabs 1 = 1
@[simp]
theorem abs_nonneg {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
0 |a|
@[simp]
theorem one_le_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
1 mabs a
@[simp]
theorem abs_abs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
|(|a|)| = |a|
@[simp]
theorem mabs_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
mabs (mabs a) = mabs a
theorem abs_add_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
|a + b| |a| + |b|

The absolute value satisfies the triangle inequality.

theorem mabs_mul_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
mabs (a * b) mabs a * mabs b

The absolute value satisfies the triangle inequality.

theorem abs_abs_sub_abs_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
||a| - |b|| |a - b|
theorem mabs_mabs_div_mabs_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
mabs (mabs a / mabs b) mabs (a / b)
theorem sup_sub_inf_eq_abs_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
a b - a b = |b - a|
theorem sup_div_inf_eq_mabs_div {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
(a b) / (a b) = mabs (b / a)
theorem two_nsmul_sup_eq_add_add_abs_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
2 (a b) = a + b + |b - a|
theorem sup_sq_eq_mul_mul_mabs_div {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
(a b) ^ 2 = a * b * mabs (b / a)
theorem two_nsmul_inf_eq_add_sub_abs_sub {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
2 (a b) = a + b - |b - a|
theorem inf_sq_eq_mul_div_mabs_div {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
(a b) ^ 2 = a * b / mabs (b / a)
theorem abs_sub_sup_add_abs_sub_inf {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
|a c - b c| + |a c - b c| = |a - b|
theorem mabs_div_sup_mul_mabs_div_inf {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
mabs ((a c) / (b c)) * mabs ((a c) / (b c)) = mabs (a / b)
theorem abs_sup_sub_sup_le_abs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
|a c - b c| |a - b|
theorem mabs_sup_div_sup_le_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
mabs ((a c) / (b c)) mabs (a / b)
theorem abs_inf_sub_inf_le_abs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
|a c - b c| |a - b|
theorem mabs_inf_div_inf_le_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
mabs ((a c) / (b c)) mabs (a / b)
theorem Birkhoff_inequalities {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
|a c - b c| |a c - b c| |a - b|
theorem m_Birkhoff_inequalities {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) (c : α) :
mabs ((a c) / (b c)) mabs ((a c) / (b c)) mabs (a / b)
theorem abs_choice {α : Type u_1} [] [] (x : α) :
|x| = x |x| = -x
theorem mabs_choice {α : Type u_1} [] [] (x : α) :
mabs x = x mabs x = x⁻¹
theorem le_abs {α : Type u_1} [] [] {a : α} {b : α} :
a |b| a b a -b
theorem le_mabs {α : Type u_1} [] [] {a : α} {b : α} :
a mabs b a b a b⁻¹
theorem abs_eq_max_neg {α : Type u_1} [] [] {a : α} :
|a| = max a (-a)
theorem mabs_eq_max_inv {α : Type u_1} [] [] {a : α} :
theorem lt_abs {α : Type u_1} [] [] {a : α} {b : α} :
a < |b| a < b a < -b
theorem lt_mabs {α : Type u_1} [] [] {a : α} {b : α} :
a < mabs b a < b a < b⁻¹
theorem abs_by_cases {α : Type u_1} [] [] {a : α} (P : αProp) (h1 : P a) (h2 : P (-a)) :
P |a|
theorem mabs_by_cases {α : Type u_1} [] [] {a : α} (P : αProp) (h1 : P a) (h2 : P a⁻¹) :
P (mabs a)
theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [] [] {a : α} {b : α} (h : |a| = b) :
a = b a = -b
theorem eq_or_eq_inv_of_mabs_eq {α : Type u_1} [] [] {a : α} {b : α} (h : mabs a = b) :
a = b a = b⁻¹
theorem abs_eq_abs {α : Type u_1} [] [] {a : α} {b : α} :
|a| = |b| a = b a = -b
theorem mabs_eq_mabs {α : Type u_1} [] [] {a : α} {b : α} :
mabs a = mabs b a = b a = b⁻¹
theorem even_abs {α : Type u_1} [] [] {a : α} :
Even |a| Even a
theorem isSquare_mabs {α : Type u_1} [] [] {a : α} :
theorem lt_of_abs_lt {α : Type u_1} [] [] {a : α} {b : α} :
|a| < ba < b
theorem lt_of_mabs_lt {α : Type u_1} [] [] {a : α} {b : α} :
mabs a < ba < b
@[simp]
theorem abs_pos {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} :
0 < |a| a 0
@[simp]
theorem one_lt_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} :
1 < mabs a a 1
theorem abs_pos_of_pos {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 0 < a) :
0 < |a|
theorem one_lt_mabs_pos_of_one_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : 1 < a) :
1 < mabs a
theorem abs_pos_of_neg {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a < 0) :
0 < |a|
theorem one_lt_mabs_of_lt_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} (h : a < 1) :
1 < mabs a
theorem neg_abs_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
-|a| a
theorem inv_mabs_le {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
theorem add_abs_nonneg {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
0 a + |a|
theorem one_le_mul_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
1 a * mabs a
theorem neg_abs_le_neg {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
-|a| -a
theorem inv_mabs_le_inv {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
theorem abs_ne_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
|a| 0 a 0
theorem mabs_ne_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
mabs a 1 a 1
@[simp]
theorem abs_eq_zero {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
|a| = 0 a = 0
@[simp]
theorem mabs_eq_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
mabs a = 1 a = 1
@[simp]
theorem abs_nonpos_iff {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
|a| 0 a = 0
@[simp]
theorem mabs_le_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
mabs a 1 a = 1
theorem abs_le_abs_of_nonpos {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (ha : a 0) (hab : b a) :
|a| |b|
theorem mabs_le_mabs_of_le_one {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (ha : a 1) (hab : b a) :
theorem abs_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] :
|a| < b -b < a a < b
theorem mabs_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] :
mabs a < b b⁻¹ < a a < b
theorem neg_lt_of_abs_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (h : |a| < b) :
-b < a
theorem inv_lt_of_mabs_lt {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (h : mabs a < b) :
b⁻¹ < a
theorem max_sub_min_eq_abs' {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
max a b - min a b = |a - b|
theorem max_div_min_eq_mabs' {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
max a b / min a b = mabs (a / b)
theorem max_sub_min_eq_abs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
max a b - min a b = |b - a|
theorem max_div_min_eq_mabs {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) (b : α) :
max a b / min a b = mabs (b / a)
def LatticeOrderedAddCommGroup.IsSolid {α : Type u_1} [] [] (s : Set α) :

A set s in a lattice ordered group is solid if for all x ∈ s and all y ∈ α such that |y| ≤ |x|, then y ∈ s.

Equations
• = ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, |y| |x|y s
Instances For
def LatticeOrderedAddCommGroup.solidClosure {α : Type u_1} [] [] (s : Set α) :
Set α

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

Equations
• = {y : α | ∃ (x : α), x s |y| |x|}
Instances For
theorem LatticeOrderedAddCommGroup.solidClosure_min {α : Type u_1} [] [] {s : Set α} {t : Set α} (hst : s t) :
@[simp]
theorem Pi.abs_apply {ι : Type u_2} {α : ιType u_3} [(i : ι) → AddGroup (α i)] [(i : ι) → Lattice (α i)] (f : (i : ι) → α i) (i : ι) :
|f| i = |f i|
theorem Pi.abs_def {ι : Type u_2} {α : ιType u_3} [(i : ι) → AddGroup (α i)] [(i : ι) → Lattice (α i)] (f : (i : ι) → α i) :
|f| = fun (i : ι) => |f i|
@[deprecated neg_le_abs]
theorem neg_le_abs_self {α : Type u_1} [] [] (a : α) :
-a |a|

Alias of neg_le_abs.

@[deprecated neg_abs_le]
theorem neg_abs_le_self {α : Type u_1} [] [] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
-|a| a

Alias of neg_abs_le.