Documentation

Mathlib.Algebra.Order.Group.Abs

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 #

def abs {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
α

abs a is the absolute value of a

Equations
Instances For
    def mabs {α : Type u_1} [Lattice α] [Group α] (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} [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 : α) :
              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) :
              @[simp]
              theorem abs_neg {α : Type u_1} [Lattice α] [AddGroup α] (a : α) :
              |(-a)| = |a|
              @[simp]
              theorem mabs_inv {α : Type u_1} [Lattice α] [Group α] (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) :
              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) :
              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) :
              @[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 : α} :
              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 : α) :
              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 : α) :
              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) :
              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| < ba < b
              theorem lt_of_mabs_lt {α : Type u_1} [Group α] [LinearOrder α] {a : α} {b : α} :
              mabs a < ba < 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|

              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
              Instances For

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

                Equations
                Instances For
                  @[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.