Absolute values in ordered groups. #
theorem
abs_by_cases
{α : Type u_1}
[inst : Neg α]
[inst : LinearOrder α]
(P : α → Prop)
{a : α}
(h1 : P a)
(h2 : P (-a))
:
P (abs 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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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 : α)
:
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 : α)
:
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 : α)
:
@[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 : α}
:
@[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 : α}
:
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)
:
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]
:
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)
:
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 : α)
:
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 : α)
:
theorem
neg_le_of_abs_le
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
(h : abs a ≤ b)
:
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))
:
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))
:
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 : α)
:
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 : α)
:
theorem
sub_le_of_abs_sub_le_left
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
{c : α}
(h : abs (a - b) ≤ c)
:
theorem
sub_le_of_abs_sub_le_right
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
{c : α}
(h : abs (a - b) ≤ c)
:
theorem
sub_lt_of_abs_sub_lt_left
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
{c : α}
(h : abs (a - b) < c)
:
theorem
sub_lt_of_abs_sub_lt_right
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
{c : α}
(h : abs (a - b) < c)
:
theorem
eq_of_abs_sub_eq_zero
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
(h : abs (a - b) = 0)
:
a = b
theorem
eq_of_abs_sub_nonpos
{α : Type u_1}
[inst : LinearOrderedAddCommGroup α]
{a : α}
{b : α}
(h : abs (a - b) ≤ 0)
:
a = b