Absolute values in ordered groups. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
abs_eq_max_neg
{α : Type u_1}
[has_neg α]
[linear_order α]
{a : α} :
|a| = linear_order.max a (-a)
theorem
abs_by_cases
{α : Type u_1}
[has_neg α]
[linear_order α]
(P : α → Prop)
{a : α}
(h1 : P a)
(h2 : P (-a)) :
theorem
abs_of_nonneg
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(h : 0 ≤ a) :
theorem
abs_of_pos
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(h : 0 < a) :
theorem
abs_of_nonpos
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(h : a ≤ 0) :
theorem
abs_of_neg
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(h : a < 0) :
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] :
@[simp]
theorem
abs_pos
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α} :
theorem
abs_pos_of_pos
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α}
(h : 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) :
theorem
neg_abs_le_self
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
theorem
add_abs_nonneg
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
(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 : α) :
@[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 : α} :
@[simp]
theorem
abs_nonpos_iff
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
{a : α} :
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] :
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) :
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
max_sub_min_eq_abs'
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a b : α) :
linear_order.max a b - linear_order.min a b = |a - b|
theorem
max_sub_min_eq_abs
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a b : α) :
linear_order.max a b - linear_order.min 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)) :
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)) :
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 : α) :
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 : α) :
theorem
sub_le_of_abs_sub_le_left
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b c : α}
(h : |a - b| ≤ c) :
theorem
sub_le_of_abs_sub_le_right
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b c : α}
(h : |a - b| ≤ c) :
theorem
sub_lt_of_abs_sub_lt_left
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b c : α}
(h : |a - b| < c) :
theorem
sub_lt_of_abs_sub_lt_right
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b c : α}
(h : |a - b| < c) :
theorem
abs_le_max_abs_abs
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b c : α}
(hab : a ≤ b)
(hbc : b ≤ c) :
theorem
min_abs_abs_le_abs_max
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α} :
linear_order.min |a| |b| ≤ |linear_order.max a b|
theorem
min_abs_abs_le_abs_min
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α} :
linear_order.min |a| |b| ≤ |linear_order.min a b|
theorem
abs_max_le_max_abs_abs
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α} :
|linear_order.max a b| ≤ linear_order.max |a| |b|
theorem
abs_min_le_max_abs_abs
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α} :
|linear_order.min a b| ≤ linear_order.max |a| |b|
theorem
eq_of_abs_sub_eq_zero
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α}
(h : |a - b| = 0) :
a = b
theorem
eq_of_abs_sub_nonpos
{α : Type u_1}
[linear_ordered_add_comm_group α]
{a b : α}
(h : |a - b| ≤ 0) :
a = b