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 #
|a|
: The absolute value of an elementa
of an additive lattice ordered group|a|ₘ
: The absolute value of an elementa
of a multiplicative lattice ordered group
theorem
apply_abs_le_mul_of_one_le'
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{β : Type u_2}
[MulOneClass β]
[Preorder β]
[MulLeftMono β]
[MulRightMono β]
{f : α → β}
{a : α}
(h₁ : 1 ≤ f a)
(h₂ : 1 ≤ f (-a))
:
theorem
apply_abs_le_add_of_nonneg'
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{β : Type u_2}
[AddZeroClass β]
[Preorder β]
[AddLeftMono β]
[AddRightMono β]
{f : α → β}
{a : α}
(h₁ : 0 ≤ f a)
(h₂ : 0 ≤ f (-a))
:
theorem
apply_abs_le_mul_of_one_le
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{β : Type u_2}
[MulOneClass β]
[Preorder β]
[MulLeftMono β]
[MulRightMono β]
{f : α → β}
(h : ∀ (x : α), 1 ≤ f x)
(a : α)
:
theorem
apply_abs_le_add_of_nonneg
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{β : Type u_2}
[AddZeroClass β]
[Preorder β]
[AddLeftMono β]
[AddRightMono β]
{f : α → β}
(h : ∀ (x : α), 0 ≤ f x)
(a : α)
:
theorem
sub_le_of_abs_sub_le_left
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b c : α}
(h : |a - b| ≤ c)
:
theorem
sub_le_of_abs_sub_le_right
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b c : α}
(h : |a - b| ≤ c)
:
theorem
sub_lt_of_abs_sub_lt_left
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b c : α}
(h : |a - b| < c)
:
theorem
sub_lt_of_abs_sub_lt_right
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b c : α}
(h : |a - b| < c)
:
theorem
eq_of_abs_sub_eq_zero
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b : α}
(h : |a - b| = 0)
:
theorem
eq_of_abs_sub_nonpos
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{a b : α}
(h : |a - b| ≤ 0)
:
theorem
eq_of_abs_sub_lt_all
{α : Type u_1}
[LinearOrderedAddCommGroup α]
{x y : α}
(h : ∀ (ε : α), ε > 0 → |x - y| < ε)
:
theorem
eq_of_abs_sub_le_all
{α : Type u_1}
[LinearOrderedAddCommGroup α]
[DenselyOrdered α]
{x y : α}
(h : ∀ (ε : α), ε > 0 → |x - y| ≤ ε)
:
@[simp]
@[simp]