Documentation

Mathlib.Algebra.Order.Group.Abs

Absolute values in ordered groups. #

instance Neg.toHasAbs {α : Type u_1} [inst : Neg α] [inst : Sup α] :
Abs α

abs a is the absolute value of a

Equations
  • Neg.toHasAbs = { abs := fun a => a -a }
instance Inv.toHasAbs {α : Type u_1} [inst : Inv α] [inst : Sup α] :
Abs α

abs a is the absolute value of a.

Equations
  • Inv.toHasAbs = { abs := fun a => a a⁻¹ }
theorem abs_eq_sup_neg {α : Type u_1} [inst : Neg α] [inst : Sup α] (a : α) :
abs a = a -a
theorem abs_eq_sup_inv {α : Type u_1} [inst : Inv α] [inst : Sup α] (a : α) :
abs a = a a⁻¹
theorem abs_eq_max_neg {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} :
abs a = max a (-a)
theorem abs_choice {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (x : α) :
abs x = x abs x = -x
theorem abs_le' {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :
abs a b a b -a b
theorem le_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :
a abs b a b a -b
theorem le_abs_self {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (a : α) :
a abs a
theorem neg_le_abs_self {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (a : α) :
-a abs a
theorem lt_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} :
a < abs b a < b a < -b
theorem abs_le_abs {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] {a : α} {b : α} (h₀ : a b) (h₁ : -a b) :
abs a abs b
theorem abs_by_cases {α : Type u_1} [inst : Neg α] [inst : LinearOrder α] (P : αProp) {a : α} (h1 : P a) (h2 : P (-a)) :
P (abs a)
@[simp]
theorem abs_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] (a : α) :
abs (-a) = abs a
theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] {a : α} {b : α} (h : abs a = b) :
a = b a = -b
theorem abs_eq_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] {a : α} {b : α} :
abs a = abs b a = b a = -b
theorem abs_sub_comm {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] (a : α) (b : α) :
abs (a - b) = abs (b - a)
theorem abs_of_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 a) :
abs a = a
theorem abs_of_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 < a) :
abs a = a
theorem abs_of_nonpos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : a 0) :
abs a = -a
theorem abs_of_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : a < 0) :
abs a = -a
theorem abs_le_abs_of_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} (ha : 0 a) (hab : a b) :
abs a abs b
@[simp]
theorem abs_zero {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] :
abs 0 = 0
@[simp]
theorem abs_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
0 < abs a a 0
theorem abs_pos_of_pos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 < a) :
0 < abs a
theorem abs_pos_of_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : a < 0) :
0 < abs a
theorem neg_abs_le_self {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) :
-abs a a
theorem add_abs_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) :
0 a + abs a
theorem neg_abs_le_neg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) :
@[simp]
theorem abs_nonneg {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) :
0 abs a
@[simp]
theorem abs_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) :
abs (abs a) = abs a
@[simp]
theorem abs_eq_zero {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
abs a = 0 a = 0
@[simp]
theorem abs_nonpos_iff {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
abs a 0 a = 0
theorem abs_le_abs_of_nonpos {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (ha : a 0) (hab : b a) :
abs a abs b
theorem abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
abs a < b -b < a a < b
theorem neg_lt_of_abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (h : abs a < b) :
-b < a
theorem lt_of_abs_lt {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (h : abs a < b) :
a < b
theorem max_sub_min_eq_abs' {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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 = abs (a - b)
theorem max_sub_min_eq_abs {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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 = abs (b - a)
theorem abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
abs a b -b a a b
theorem le_abs' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
a abs b b -a a b
theorem neg_le_of_abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs a b) :
-b a
theorem le_of_abs_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs a b) :
a b
theorem apply_abs_le_add_of_nonneg' {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : AddZeroClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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 (abs a) f a + f (-a)
theorem apply_abs_le_mul_of_one_le' {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : MulOneClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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 (abs a) f a * f (-a)
theorem apply_abs_le_add_of_nonneg {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : AddZeroClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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 (abs a) f a + f (-a)
theorem apply_abs_le_mul_of_one_le {α : Type u_2} [inst : LinearOrderedAddCommGroup α] {β : Type u_1} [inst : MulOneClass β] [inst : Preorder β] [inst : CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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 (abs a) f a * f (-a)
theorem abs_add {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs (a + b) abs a + abs b

The triangle inequality in LinearOrderedAddCommGroups.

theorem abs_add' {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs a abs b + abs (b + a)
theorem abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs (a - b) abs a + abs b
theorem abs_sub_le_iff {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} :
abs (a - b) c a - b c b - a c
theorem abs_sub_lt_iff {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} :
abs (a - b) < c a - b < c b - a < c
theorem sub_le_of_abs_sub_le_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) c) :
b - c a
theorem sub_le_of_abs_sub_le_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) c) :
a - c b
theorem sub_lt_of_abs_sub_lt_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) < c) :
b - c < a
theorem sub_lt_of_abs_sub_lt_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (h : abs (a - b) < c) :
a - c < b
theorem abs_sub_abs_le_abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs a - abs b abs (a - b)
theorem abs_abs_sub_abs_le_abs_sub {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
abs (abs a - abs b) abs (a - b)
theorem abs_eq {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (hb : 0 b) :
abs a = b a = b a = -b
theorem abs_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {c : α} (hab : a b) (hbc : b c) :
abs b max (abs a) (abs c)
theorem min_abs_abs_le_abs_max {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
min (abs a) (abs b) abs (max a b)
theorem min_abs_abs_le_abs_min {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
min (abs a) (abs b) abs (min a b)
theorem abs_max_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
abs (max a b) max (abs a) (abs b)
theorem abs_min_le_max_abs_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} :
abs (min a b) max (abs a) (abs b)
theorem eq_of_abs_sub_eq_zero {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs (a - b) = 0) :
a = b
theorem abs_sub_le {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
abs (a - c) abs (a - b) + abs (b - c)
theorem abs_add_three {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
abs (a + b + c) abs a + abs b + abs c
theorem dist_bdd_within_interval {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} {lb : α} {ub : α} (hal : lb a) (hau : a ub) (hbl : lb b) (hbu : b ub) :
abs (a - b) ub - lb
theorem eq_of_abs_sub_nonpos {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} {b : α} (h : abs (a - b) 0) :
a = b