mathlib3 documentation

algebra.order.group.abs

Absolute values in ordered groups. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def has_neg.to_has_abs {α : Type u_1} [has_neg α] [has_sup α] :

abs a is the absolute value of a

Equations
@[protected, instance]
def has_inv.to_has_abs {α : Type u_1} [has_inv α] [has_sup α] :

abs a is the absolute value of a.

Equations
theorem abs_eq_sup_inv {α : Type u_1} [has_inv α] [has_sup α] (a : α) :
theorem abs_eq_sup_neg {α : Type u_1} [has_neg α] [has_sup α] (a : α) :
|a| = a -a
theorem abs_eq_max_neg {α : Type u_1} [has_neg α] [linear_order α] {a : α} :
theorem abs_choice {α : Type u_1} [has_neg α] [linear_order α] (x : α) :
|x| = x |x| = -x
theorem abs_le' {α : Type u_1} [has_neg α] [linear_order α] {a b : α} :
|a| b a b -a b
theorem le_abs {α : Type u_1} [has_neg α] [linear_order α] {a b : α} :
a |b| a b a -b
theorem le_abs_self {α : Type u_1} [has_neg α] [linear_order α] (a : α) :
a |a|
theorem neg_le_abs_self {α : Type u_1} [has_neg α] [linear_order α] (a : α) :
-a |a|
theorem lt_abs {α : Type u_1} [has_neg α] [linear_order α] {a b : α} :
a < |b| a < b a < -b
theorem abs_le_abs {α : Type u_1} [has_neg α] [linear_order α] {a b : α} (h₀ : a b) (h₁ : -a b) :
theorem abs_by_cases {α : Type u_1} [has_neg α] [linear_order α] (P : α Prop) {a : α} (h1 : P a) (h2 : P (-a)) :
P |a|
@[simp]
theorem abs_neg {α : Type u_1} [add_group α] [linear_order α] (a : α) :
|-a| = |a|
theorem eq_or_eq_neg_of_abs_eq {α : Type u_1} [add_group α] [linear_order α] {a b : α} (h : |a| = b) :
a = b a = -b
theorem abs_eq_abs {α : Type u_1} [add_group α] [linear_order α] {a b : α} :
|a| = |b| a = b a = -b
theorem abs_sub_comm {α : Type u_1} [add_group α] [linear_order α] (a b : α) :
|a - b| = |b - a|
theorem abs_of_nonneg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 a) :
|a| = a
theorem abs_of_pos {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 < a) :
|a| = a
theorem abs_of_nonpos {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a 0) :
|a| = -a
theorem abs_of_neg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a < 0) :
|a| = -a
theorem abs_le_abs_of_nonneg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} (ha : 0 a) (hab : a b) :
@[simp]
theorem abs_zero {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] :
|0| = 0
@[simp]
theorem abs_pos {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 < |a| a 0
theorem abs_pos_of_pos {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 < a) :
0 < |a|
theorem abs_pos_of_neg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a < 0) :
0 < |a|
theorem neg_abs_le_self {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
-|a| a
theorem add_abs_nonneg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
0 a + |a|
theorem neg_abs_le_neg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
@[simp]
theorem abs_nonneg {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
0 |a|
@[simp]
theorem abs_abs {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
@[simp]
theorem abs_eq_zero {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| = 0 a = 0
@[simp]
theorem abs_nonpos_iff {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| 0 a = 0
theorem abs_le_abs_of_nonpos {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] (ha : a 0) (hab : b a) :
theorem abs_lt {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] :
|a| < b -b < a a < b
theorem neg_lt_of_abs_lt {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] (h : |a| < b) :
-b < a
theorem lt_of_abs_lt {α : Type u_1} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] (h : |a| < b) :
a < b
theorem abs_le {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} :
|a| b -b a a b
theorem le_abs' {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} :
a |b| b -a a b
theorem neg_le_of_abs_le {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (h : |a| b) :
-b a
theorem le_of_abs_le {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (h : |a| b) :
a b
theorem apply_abs_le_mul_of_one_le' {α : Type u_1} [linear_ordered_add_comm_group α] {β : Type u_2} [mul_one_class β] [preorder β] [covariant_class β β has_mul.mul has_le.le] [covariant_class β β (function.swap has_mul.mul) has_le.le] {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} [linear_ordered_add_comm_group α] {β : Type u_2} [add_zero_class β] [preorder β] [covariant_class β β has_add.add has_le.le] [covariant_class β β (function.swap has_add.add) has_le.le] {f : α β} {a : α} (h₁ : 0 f a) (h₂ : 0 f (-a)) :
f |a| f a + f (-a)
theorem apply_abs_le_add_of_nonneg {α : Type u_1} [linear_ordered_add_comm_group α] {β : Type u_2} [add_zero_class β] [preorder β] [covariant_class β β has_add.add has_le.le] [covariant_class β β (function.swap has_add.add) has_le.le] {f : α β} (h : (x : α), 0 f x) (a : α) :
f |a| f a + f (-a)
theorem apply_abs_le_mul_of_one_le {α : Type u_1} [linear_ordered_add_comm_group α] {β : Type u_2} [mul_one_class β] [preorder β] [covariant_class β β has_mul.mul has_le.le] [covariant_class β β (function.swap has_mul.mul) has_le.le] {f : α β} (h : (x : α), 1 f x) (a : α) :
f |a| f a * f (-a)
theorem abs_add {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
|a + b| |a| + |b|

The triangle inequality in linear_ordered_add_comm_groups.

theorem abs_add' {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
|a| |b| + |b + a|
theorem abs_sub {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
|a - b| |a| + |b|
theorem abs_sub_le_iff {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} :
|a - b| c a - b c b - a c
theorem abs_sub_lt_iff {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} :
|a - b| < c a - b < c b - a < c
theorem sub_le_of_abs_sub_le_left {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : |a - b| c) :
b - c a
theorem sub_le_of_abs_sub_le_right {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : |a - b| c) :
a - c b
theorem sub_lt_of_abs_sub_lt_left {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : |a - b| < c) :
b - c < a
theorem sub_lt_of_abs_sub_lt_right {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (h : |a - b| < c) :
a - c < b
theorem abs_sub_abs_le_abs_sub {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
|a| - |b| |a - b|
theorem abs_abs_sub_abs_le_abs_sub {α : Type u_1} [linear_ordered_add_comm_group α] (a b : α) :
||a| - |b|| |a - b|
theorem abs_eq {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (hb : 0 b) :
|a| = b a = b a = -b
theorem abs_le_max_abs_abs {α : Type u_1} [linear_ordered_add_comm_group α] {a b c : α} (hab : a b) (hbc : b c) :
theorem eq_of_abs_sub_eq_zero {α : Type u_1} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| = 0) :
a = b
theorem abs_sub_le {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
|a - c| |a - b| + |b - c|
theorem abs_add_three {α : Type u_1} [linear_ordered_add_comm_group α] (a b c : α) :
|a + b + c| |a| + |b| + |c|
theorem dist_bdd_within_interval {α : Type u_1} [linear_ordered_add_comm_group α] {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} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| 0) :
a = b