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} [Lattice α] [AddGroup α] (a : α) : α

abs a is the absolute value of a

Equations

• |a| = a ⊔ -a

def mabs {α : Type u_1} [Lattice α] [Group α] (a : α) : α

mabs a is the absolute value of a.

Equations

• mabs a = a ⊔ a⁻¹

def «term|___|ₘ» : Lean.ParserDescr

mabs a is the absolute value of a.

Equations

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

def «term|___|» : Lean.ParserDescr

abs a is the absolute value of a

Equations

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

def mabs.unexpander : Lean.PrettyPrinter.Unexpander

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.

def abs.unexpander : Lean.PrettyPrinter.Unexpander

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.

theorem abs_le' {α : Type u_1} [Lattice α] [AddGroup α] {a : α} {b : α} : |a| ≤ b ↔ a ≤ b ∧ -a ≤ b

theorem mabs_le' {α : Type u_1} [Lattice α] [Group α] {a : α} {b : α} : mabs a ≤ b ↔ a ≤ b ∧ a⁻¹ ≤ b

theorem le_abs_self {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : a ≤ |a|

theorem le_mabs_self {α : Type u_1} [Lattice α] [Group α] (a : α) : a ≤ mabs a

theorem neg_le_abs {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : -a ≤ |a|

theorem inv_le_mabs {α : Type u_1} [Lattice α] [Group α] (a : α) : a⁻¹ ≤ mabs a

theorem abs_le_abs {α : Type u_1} [Lattice α] [AddGroup α] {a : α} {b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) : |a| ≤ |b|

theorem mabs_le_mabs {α : Type u_1} [Lattice α] [Group α] {a : α} {b : α} (h₀ : a ≤ b) (h₁ : a⁻¹ ≤ b) : mabs a ≤ mabs b

@[simp]

theorem abs_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) : |(-a)| = |a|

@[simp]

theorem mabs_inv {α : Type u_1} [Lattice α] [Group α] (a : α) : mabs a⁻¹ = mabs a

theorem abs_sub_comm {α : Type u_1} [Lattice α] [AddGroup α] (a : α) (b : α) : |a - b| = |b - a|

theorem mabs_div_comm {α : Type u_1} [Lattice α] [Group α] (a : α) (b : α) : mabs (a / b) = mabs (b / a)

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

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

theorem abs_of_pos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : 0 < a) : |a| = a

theorem mabs_of_one_lt {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (h : 1 < a) : mabs a = a

theorem abs_of_nonpos {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : a ≤ 0) : |a| = -a

theorem mabs_of_le_one {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (h : a ≤ 1) : mabs a = a⁻¹

theorem abs_of_neg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : a < 0) : |a| = -a

theorem mabs_of_lt_one {α : Type u_1} [Lattice α] [Group α] {a : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (h : a < 1) : mabs a = a⁻¹

theorem abs_le_abs_of_nonneg {α : Type u_1} [Lattice α] [AddGroup α] {a : α} {b : α} [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (ha : 0 ≤ a) (hab : a ≤ b) : |a| ≤ |b|

theorem mabs_le_mabs_of_one_le {α : Type u_1} [Lattice α] [Group α] {a : α} {b : α} [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (ha : 1 ≤ a) (hab : a ≤ b) : mabs a ≤ mabs b

@[simp]

theorem abs_zero {α : Type u_1} [Lattice α] [AddGroup α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : |0| = 0

@[simp]

theorem mabs_one {α : Type u_1} [Lattice α] [Group α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : mabs 1 = 1

@[simp]

theorem abs_nonneg {α : 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 : α) : 0 ≤ |a|

@[simp]

theorem one_le_mabs {α : 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 : α) : 1 ≤ mabs a

@[simp]

theorem abs_abs {α : 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 : α) : |(|a|)| = |a|

@[simp]

theorem mabs_mabs {α : 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 : α) : mabs (mabs a) = mabs a

theorem abs_add_le {α : 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|

The absolute value satisfies the triangle inequality.

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

theorem mabs_mabs_div_mabs_le {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : mabs (mabs a / mabs b) ≤ mabs (a / b)

theorem sup_sub_inf_eq_abs_sub {α : 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 = |b - a|

theorem sup_div_inf_eq_mabs_div {α : 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) = mabs (b / a)

theorem two_nsmul_sup_eq_add_add_abs_sub {α : Type u_1} [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 sup_sq_eq_mul_mul_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : (a ⊔ b) ^ 2 = a * b * mabs (b / a)

theorem two_nsmul_inf_eq_add_sub_abs_sub {α : Type u_1} [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 inf_sq_eq_mul_div_mabs_div {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : (a ⊓ b) ^ 2 = a * b / mabs (b / a)

theorem abs_sub_sup_add_abs_sub_inf {α : Type u_1} [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 mabs_div_sup_mul_mabs_div_inf {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (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} [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 mabs_sup_div_sup_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) : mabs ((a ⊔ c) / (b ⊔ c)) ≤ mabs (a / b)

theorem abs_inf_sub_inf_le_abs {α : Type u_1} [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 mabs_inf_div_inf_le_mabs {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) : mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)

theorem Birkhoff_inequalities {α : Type u_1} [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 m_Birkhoff_inequalities {α : Type u_1} [Lattice α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) (c : α) : mabs ((a ⊔ c) / (b ⊔ c)) ⊔ mabs ((a ⊓ c) / (b ⊓ c)) ≤ mabs (a / b)

theorem abs_choice {α : Type u_1} [AddGroup α] [LinearOrder α] (x : α) : |x| = x ∨ |x| = -x

theorem mabs_choice {α : Type u_1} [Group α] [LinearOrder α] (x : α) : mabs x = x ∨ mabs x = x⁻¹

theorem le_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} {b : α} : a ≤ |b| ↔ a ≤ b ∨ a ≤ -b

theorem le_mabs {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} : a ≤ mabs b ↔ a ≤ b ∨ a ≤ b⁻¹

theorem abs_eq_max_neg {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} : |a| = max a (-a)

theorem mabs_eq_max_inv {α : Type u_1} [Group α] [LinearOrder α] {a : α} : mabs a = max a a⁻¹

theorem lt_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} {b : α} : a < |b| ↔ a < b ∨ a < -b

theorem lt_mabs {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} : a < mabs b ↔ a < b ∨ a < b⁻¹

theorem abs_by_cases {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} (P : α → Prop) (h1 : P a) (h2 : P (-a)) : P |a|

theorem mabs_by_cases {α : Type u_1} [Group α] [LinearOrder α] {a : α} (P : α → Prop) (h1 : P a) (h2 : P a⁻¹) : P (mabs a)

theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} {b : α} (h : |a| = b) : a = b ∨ a = -b

theorem eq_or_eq_inv_of_mabs_eq {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} (h : mabs a = b) : a = b ∨ a = b⁻¹

theorem abs_eq_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} {b : α} : |a| = |b| ↔ a = b ∨ a = -b

theorem mabs_eq_mabs {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} : mabs a = mabs b ↔ a = b ∨ a = b⁻¹

@[simp]

theorem abs_pos {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : 0 < |a| ↔ a ≠ 0

@[simp]

theorem one_lt_mabs {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} : 1 < mabs a ↔ a ≠ 1

theorem abs_pos_of_pos {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (h : 0 < a) : 0 < |a|

theorem one_lt_mabs_pos_of_one_lt {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (h : 1 < a) : 1 < mabs a

theorem abs_pos_of_neg {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (h : a < 0) : 0 < |a|

theorem one_lt_mabs_of_lt_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} (h : a < 1) : 1 < mabs a

theorem neg_abs_le {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : -|a| ≤ a

theorem inv_mabs_le {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : (mabs a)⁻¹ ≤ a

theorem add_abs_nonneg {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : 0 ≤ a + |a|

theorem one_le_mul_mabs {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : 1 ≤ a * mabs a

theorem neg_abs_le_neg {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : -|a| ≤ -a

theorem inv_mabs_le_inv {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : (mabs a)⁻¹ ≤ a⁻¹

theorem abs_ne_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : |a| ≠ 0 ↔ a ≠ 0

theorem mabs_ne_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : mabs a ≠ 1 ↔ a ≠ 1

@[simp]

theorem abs_eq_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : |a| = 0 ↔ a = 0

@[simp]

theorem mabs_eq_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : mabs a = 1 ↔ a = 1

@[simp]

theorem abs_nonpos_iff {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : |a| ≤ 0 ↔ a = 0

@[simp]

theorem mabs_le_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : mabs a ≤ 1 ↔ a = 1

theorem abs_le_abs_of_nonpos {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (ha : a ≤ 0) (hab : b ≤ a) : |a| ≤ |b|

theorem mabs_le_mabs_of_le_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (ha : a ≤ 1) (hab : b ≤ a) : mabs a ≤ mabs b

theorem abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : |a| < b ↔ -b < a ∧ a < b

theorem mabs_lt {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : mabs a < b ↔ b⁻¹ < a ∧ a < b

theorem neg_lt_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (h : |a| < b) : -b < a

theorem inv_lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] {a : α} {b : α} [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (h : mabs a < b) : b⁻¹ < a

theorem lt_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] {a : α} {b : α} : |a| < b → a < b

theorem lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} : mabs a < b → a < b

theorem max_sub_min_eq_abs' {α : Type u_1} [AddGroup α] [LinearOrder α] [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 : α) : max a b - min a b = |a - b|

theorem max_div_min_eq_mabs' {α : Type u_1} [Group α] [LinearOrder α] [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 : α) : max a b / min a b = mabs (a / b)

theorem max_sub_min_eq_abs {α : Type u_1} [AddGroup α] [LinearOrder α] [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 : α) : max a b - min a b = |b - a|

theorem max_div_min_eq_mabs {α : Type u_1} [Group α] [LinearOrder α] [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 : α) : max a b / min a b = mabs (b / a)

theorem abs_nsmul {α : Type u_1} [LinearOrderedAddCommGroup α] (n : ℕ) (a : α) : |n • a| = n • |a|

theorem mabs_pow {α : Type u_1} [LinearOrderedCommGroup α] (n : ℕ) (a : α) : mabs (a ^ n) = mabs a ^ n

theorem abs_add_eq_add_abs_iff {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

theorem mabs_mul_eq_mul_mabs_iff {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) : mabs (a * b) = mabs a * mabs b ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

theorem abs_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : |a| ≤ b ↔ -b ≤ a ∧ a ≤ b

theorem le_abs' {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : a ≤ |b| ↔ b ≤ -a ∨ a ≤ b

theorem neg_le_of_abs_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : |a| ≤ b) : -b ≤ a

theorem le_of_abs_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : |a| ≤ b) : a ≤ b

theorem apply_abs_le_add_of_nonneg' {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_2} [AddZeroClass β] [Preorder β] [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] {f : α → β} {a : α} (h₁ : 0 ≤ f a) (h₂ : 0 ≤ f (-a)) : f |a| ≤ f a + f (-a)

theorem apply_abs_le_mul_of_one_le' {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_2} [MulOneClass β] [Preorder β] [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] {f : α → β} {a : α} (h₁ : 1 ≤ f a) (h₂ : 1 ≤ f (-a)) : f |a| ≤ f a * f (-a)

theorem apply_abs_le_add_of_nonneg {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_2} [AddZeroClass β] [Preorder β] [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] {f : α → β} (h : ∀ (x : α), 0 ≤ f x) (a : α) : f |a| ≤ f a + f (-a)

theorem apply_abs_le_mul_of_one_le {α : Type u_1} [LinearOrderedAddCommGroup α] {β : Type u_2} [MulOneClass β] [Preorder β] [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] {f : α → β} (h : ∀ (x : α), 1 ≤ f x) (a : α) : f |a| ≤ f a * f (-a)

theorem abs_add {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a + b| ≤ |a| + |b|

The triangle inequality in LinearOrderedAddCommGroups.

theorem abs_add' {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a| ≤ |b| + |b + a|

theorem abs_sub {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a - b| ≤ |a| + |b|

theorem abs_sub_le_iff {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} : |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c

theorem abs_sub_lt_iff {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} : |a - b| < c ↔ a - b < c ∧ b - a < c

theorem sub_le_of_abs_sub_le_left {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : |a - b| ≤ c) : b - c ≤ a

theorem sub_le_of_abs_sub_le_right {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : |a - b| ≤ c) : a - c ≤ b

theorem sub_lt_of_abs_sub_lt_left {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : |a - b| < c) : b - c < a

theorem sub_lt_of_abs_sub_lt_right {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : |a - b| < c) : a - c < b

theorem abs_sub_abs_le_abs_sub {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : |a| - |b| ≤ |a - b|

theorem abs_abs_sub_abs_le_abs_sub {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : ||a| - |b|| ≤ |a - b|

theorem abs_sub_le_of_nonneg_of_le {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {n : α} (a_nonneg : 0 ≤ a) (a_le_n : a ≤ n) (b_nonneg : 0 ≤ b) (b_le_n : b ≤ n) : |a - b| ≤ n

|a - b| ≤ n if 0 ≤ a ≤ n and 0 ≤ b ≤ n.

theorem abs_sub_lt_of_nonneg_of_lt {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {n : α} (a_nonneg : 0 ≤ a) (a_lt_n : a < n) (b_nonneg : 0 ≤ b) (b_lt_n : b < n) : |a - b| < n

|a - b| < n if 0 ≤ a < n and 0 ≤ b < n.

theorem abs_eq {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (hb : 0 ≤ b) : |a| = b ↔ a = b ∨ a = -b

theorem abs_le_max_abs_abs {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b ≤ c) : |b| ≤ max |a| |c|

theorem min_abs_abs_le_abs_max {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : min |a| |b| ≤ |max a b|

theorem min_abs_abs_le_abs_min {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : min |a| |b| ≤ |min a b|

theorem abs_max_le_max_abs_abs {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : |max a b| ≤ max |a| |b|

theorem abs_min_le_max_abs_abs {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : |min a b| ≤ max |a| |b|

theorem eq_of_abs_sub_eq_zero {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : |a - b| = 0) : a = b

theorem abs_sub_le {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : |a - c| ≤ |a - b| + |b - c|

theorem abs_add_three {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : |a + b + c| ≤ |a| + |b| + |c|

theorem dist_bdd_within_interval {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} {lb : α} {ub : α} (hal : lb ≤ a) (hau : a ≤ ub) (hbl : lb ≤ b) (hbu : b ≤ ub) : |a - b| ≤ ub - lb

theorem eq_of_abs_sub_nonpos {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} (h : |a - b| ≤ 0) : a = b

theorem abs_sub_nonpos {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : |a - b| ≤ 0 ↔ a = b

theorem abs_sub_pos {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} {b : α} : 0 < |a - b| ↔ a ≠ b

@[simp]

theorem abs_eq_self {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} : |a| = a ↔ 0 ≤ a

@[simp]

theorem abs_eq_neg_self {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} : |a| = -a ↔ a ≤ 0

theorem abs_cases {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) : |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

For an element a of a linear ordered ring, either abs a = a and 0 ≤ a, or abs a = -a and a < 0. Use cases on this lemma to automate linarith in inequalities

@[simp]

theorem max_zero_add_max_neg_zero_eq_abs_self {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) : max a 0 + max (-a) 0 = |a|

def LatticeOrderedAddCommGroup.IsSolid {α : Type u_1} [Lattice α] [AddCommGroup α] (s : Set α) : Prop

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

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

def LatticeOrderedAddCommGroup.solidClosure {α : Type u_1} [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 : α), x ∈ s ∧ |y| ≤ |x|}

theorem LatticeOrderedAddCommGroup.isSolid_solidClosure {α : Type u_1} [Lattice α] [AddCommGroup α] (s : Set α) : LatticeOrderedAddCommGroup.IsSolid (LatticeOrderedAddCommGroup.solidClosure s)

theorem LatticeOrderedAddCommGroup.solidClosure_min {α : Type u_1} [Lattice α] [AddCommGroup α] {s : Set α} {t : Set α} (hst : s ⊆ t) (ht : LatticeOrderedAddCommGroup.IsSolid t) : LatticeOrderedAddCommGroup.solidClosure 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} [Lattice α] [AddGroup α] (a : α) : -a ≤ |a|

Alias of neg_le_abs.

@[deprecated neg_abs_le]

theorem neg_abs_le_self {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) : -|a| ≤ a

Alias of neg_abs_le.