le_mabs_self
theorem le_mabs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), a ≤ mabs a
The theorem `le_mabs_self` states that for any type `α` that is both a lattice and a group, any element `a` of this type is less than or equal to the absolute value of `a`. Here, the absolute value of `a`, denoted as `mabs a`, is defined as the supremum of `a` and its inverse.
More concisely: For all lattice and group types `α` and elements `a` in `α`, we have `a ≤ mabs a`, where `mabs a` is the supremum of `a` and its inverse.
|
abs_nonneg
theorem abs_nonneg :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), 0 ≤ |a|
The theorem `abs_nonneg` states that for any value `a` of a type `α`, which is a lattice and an additive group, and has both left and right covariant classes with respect to addition and order, the absolute value of `a` is always nonnegative, i.e., `0 ≤ |a|`. In mathematical terms, this can be represented as: ∀a ∈ α, 0 ≤ |a|. The covariant classes ensure that the type `α` is ordered and has properties that relate its order and its binary operation (addition in this case).
More concisely: For any element `a` in a lattice and additive group type `α` with covariant classes for addition and order, the absolute value `|a|` is nonnegative.
|
mabs_of_one_le
theorem mabs_of_one_le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], 1 ≤ a → mabs a = a
The theorem `mabs_of_one_le` states that for any type `α` that is a lattice and a group, and for any element `a` of type `α` such that the binary operation "multiplication" is covariant in both of its arguments, if `1` is less than or equal to `a`, then the absolute value of `a` (denoted `mabs a`) is equal to `a` itself. Essentially, it means that for positive elements (i.e., elements greater than or equal to 1) in this specific algebraic structure, the absolute value operation returns the element itself.
More concisely: For any lattice and group type `α` with covariant multiplication, if `1 ≤ a`, then `mabs a = a`.
|
one_le_mabs
theorem one_le_mabs :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α), 1 ≤ mabs a
The theorem `one_le_mabs` states that for any type `α` that has a lattice structure, a group structure, and satisfies two specific covariance conditions, the absolute value (`mabs`) of any element `a` of type `α` is always greater than or equal to one.
The covariance conditions are given in terms of multiplication (`x * x_1`) and an order relation (`x ≤ x_1`). The first condition requires that for any two elements `x` and `x_1` in `α`, if `x * x_1` increases, then `x` increases. The second condition requires the same but with the arguments to the multiplication operation swapped.
This is a generalization of the property we know from real numbers where the absolute value of a number is always non-negative, and is 1 for non-zero numbers when normalized with respect to the group operation.
More concisely: For any type `α` with lattice and group structures satisfying multiplicative covariance conditions `x * x_1 => x <= x_1` and `x_1 * x => x <= x_1`, the absolute value `mabs a` of any element `a` in `α` is greater than or equal to one.
|
abs_zero
theorem abs_zero :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], |0| = 0
This is a theorem stating that the absolute value of zero is zero for any type `α` that is a lattice and an additive group, and for which addition (`x + x_1`) is a covariant function in the sense that if `x ≤ y`, then `f(x) ≤ f(y)`. This holds true regardless of the specific type `α` as long as it fulfills these conditions, thus it applies to integers, real numbers, complex numbers, and many other mathematical structures.
More concisely: For any lattice and additive group type `α` where addition is covariant, the absolute value of zero is zero.
|
neg_abs_le
theorem neg_abs_le :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), -|a| ≤ a
This theorem, `neg_abs_le`, states that for any type `α` that is an additive group and linearly ordered, and for which addition is a covariant operation with respect to the order, the negative absolute value of any element `a` is less than or equal to `a` itself. In simple terms, in any linearly ordered additive group, any number is greater than or equal to its own negative absolute value.
More concisely: In a linearly ordered additive group, for all elements `a`, we have `-|a| ≤ a`. (Here, `|a|` denotes the absolute value of `a`, and `-|a|` denotes the negative absolute value.)
|
abs_sup_sub_sup_le_abs
theorem abs_sup_sub_sup_le_abs :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
|a ⊔ c - b ⊔ c| ≤ |a - b|
This theorem states that for any type `α` that is a lattice and an additive commutative group, and also has the covariance property with respect to addition and ordering, the absolute difference between the supremum (or join) of `a` and `c` and the supremum of `b` and `c` is less than or equal to the absolute difference between `a` and `b`. This means the impact of the supremum operation combined with subtraction on `a`, `b`, and `c` does not increase the absolute difference between `a` and `b`.
More concisely: For any lattice, additive commutative group `α` with covariance property for addition and ordering, |sup(a, c) - sup(b, c)| ≤ |a - b|.
|
sup_sub_inf_eq_abs_sub
theorem sup_sub_inf_eq_abs_sub :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a ⊔ b - a ⊓ b = |b - a|
The theorem `sup_sub_inf_eq_abs_sub` states that for all types `α` that form a lattice and an additive commutative group, and additionally satisfy a covariance property (specifically, for all elements `x` and `x_1` of the type, `x + x_1` implies `x ≤ x_1`), the difference between the supremum (`a ⊔ b`) and the infimum (`a ⊓ b`) of any two elements `a` and `b` of the type is equal to the absolute value of the difference between `b` and `a`.
More concisely: For all types `α` that form a lattice and an additive commutative group with the covariance property, the supremum and infimum of any two elements `a` and `b` satisfy `|a - b| = a ⊔ b - a ⊓ b`.
|
Mathlib.Algebra.Order.Group.Abs._auxLemma.2
theorem Mathlib.Algebra.Order.Group.Abs._auxLemma.2 :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α),
(0 ≤ |a|) = True
This theorem, `Mathlib.Algebra.Order.Group.Abs._auxLemma.2`, states that for any type `α`, given that `α` is a lattice and an additive group, and the addition operation "`+`" on `α` satisfies the two specified covariant classes, then the absolute value of any element `a` of type `α` is always greater than or equal to zero. The equality `(0 ≤ |a|) = True` in Lean signifies that the non-negativity of the absolute value is a universally true statement.
More concisely: If `α` is a lattice and an additive group such that the absolute value `|.|` is a non-negative, covariant norm on `α`, then for all `a ∈ α`, we have `0 ≤ |a|`.
|
abs_of_neg
theorem abs_of_neg :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a < 0 → |a| = -a
This theorem, `abs_of_neg`, states that for any type `α` that is a lattice and an add group (additive group), and for every instance `a` of this type `α`, if `a` is less than zero then the absolute value of `a` is equivalent to the negation of `a`. Note that the property of covariance is also required for the `α` elements under the operation of addition and a comparison function to guarantee the order relation.
More concisely: For any lattice and add group type `α` with covariance property, if `a` is an element of `α` and `a` is negative, then `|a| = -a`.
|
abs_pos
theorem abs_pos :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 < |a| ↔ a ≠ 0
The theorem `abs_pos` states that for any value `a` of an ordered additive group `α`, the absolute value of `a` is greater than zero if and only if `a` is not equal to zero. Here, the additive group structure on `α` satisfies the property that addition of any two elements of `α` preserves the order, i.e., if `x ≤ y` then `x + z ≤ y + z` for all `x, y, z` in `α`.
More concisely: The absolute value of an element in an ordered additive group is positive if and only if the element is non-zero.
|
eq_or_eq_neg_of_abs_eq
theorem eq_or_eq_neg_of_abs_eq :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] {a b : α}, |a| = b → a = b ∨ a = -b
This theorem states that for any type `α` that has an addition group structure and a linear order, given any two elements `a` and `b` from `α`, if the absolute value of `a` is equal to `b`, then `a` is either equal to `b` or the negative of `b`. In mathematical notation, this would be stated as: for all `a` and `b` in a linearly ordered additive group, if `|a| = b` then `a = b` or `a = -b`.
More concisely: In an additively and linearly ordered type `α`, for all `a` and `b`, if the absolute value of `a` equals `b`, then `a` is equal to `b` or the negative of `b`.
|
le_of_abs_le
theorem le_of_abs_le : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b : α}, |a| ≤ b → a ≤ b
This theorem, `le_of_abs_le`, states that for any type `α` which forms a linear ordered additive commutative group, given any two elements `a` and `b` of this type, if the absolute value of `a` is less than or equal to `b`, then `a` itself is also less than or equal to `b`. This theorem is essentially capturing the well-known property from mathematics that in any ordered group, the absolute value of a member provides an upper bound of that member.
More concisely: For all additive, commutative, and linearly ordered group types `α` and elements `a` and `b` of type `α`, if `|a| ≤ b`, then `a ≤ b`.
|
sup_div_inf_eq_mabs_div
theorem sup_div_inf_eq_mabs_div :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a b : α),
(a ⊔ b) / (a ⊓ b) = mabs (b / a)
This theorem states that for any type `α`, where `α` is a lattice and a commutative group, with a specific covariance property, and given any two elements `a` and `b` of this type `α`, the supremum (greatest lower bound) of `a` and `b` divided by the infimum (least upper bound) of `a` and `b` is equal to the absolute value of the fraction `b / a`. Here, the absolute value is defined as the supremum of an element and its inverse.
More concisely: For any commutative lattice and group type `α` with the given covariance property, the absolute value of `b/a` equals the supremum of `a` and `b` divided by the infimum of `a` and `b`.
|
abs_lt
theorem abs_lt :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
|a| < b ↔ -b < a ∧ a < b
The theorem `abs_lt` states that for any type `α` that is a linearly ordered additive group, and `a` and `b` being members of this type `α`, the absolute value of `a` is less than `b` if and only if `a` lies strictly between `-b` and `b`. Here, CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1 denotes monotonicity of addition in α, and CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1 represents that the function swap preserves the order.
More concisely: For any linearly ordered additive group `α` and `a, b ∈ α`, `|a| < |b|` if and only if `-b < a < b`.
|
abs_le'
theorem abs_le' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a b : α}, |a| ≤ b ↔ a ≤ b ∧ -a ≤ b := by
sorry
The theorem `abs_le'` states that for all types `α`, where `α` is a lattice and an additive group, and for any two elements `a` and `b` of type `α`, the absolute value of `a` is less than or equal to `b` if and only if `a` is less than or equal to `b` and `-a` is less than or equal to `b`. This theorem essentially expresses the property of absolute values in the context of lattices and additive groups.
More concisely: For all lattice and additive groups $\alpha$, and all $a, b \in \alpha$, $|a| \leq b$ if and only if $a \leq b$ and $-a \leq b$.
|
abs_sub_le_iff
theorem abs_sub_le_iff :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c : α}, |a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
This theorem states that for any type `α` that forms a Linear Ordered Additive Commutative Group, for any three elements `a`, `b`, and `c` of this type, the absolute value of the difference between `a` and `b` is less than or equal to `c` if and only if both the difference `a - b` is less than or equal to `c` and the difference `b - a` is less than or equal to `c`. In mathematical terms, we can express this as: $|a - b| \leq c$ if and only if both $a - b \leq c$ and $b - a \leq c$.
More concisely: For any type `α` forming a Linear Ordered Additive Commutative Group, $|a-b|\leq c$ if and only if $a-b\leq c$ and $b-a\leq c$.
|
mabs_of_le_one
theorem mabs_of_le_one :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], a ≤ 1 → mabs a = a⁻¹
The theorem `mabs_of_le_one` states that for any type `α` which is both a lattice and a group, and where multiplication (`*`) is a covariant operation in the sense that multiplying two elements doesn't reverse the order of the elements, if an element `a` of `α` is less than or equal to `1`, then the absolute value of `a` (as defined by the function `mabs`) is equal to the inverse of `a`.
More concisely: If `α` is a lattice and group type with covariant multiplication, then for all `a` in `α` with `0 ≤ a`, we have `mabs a = a^(-1)`.
|
Mathlib.Algebra.Order.Group.Abs._auxLemma.15
theorem Mathlib.Algebra.Order.Group.Abs._auxLemma.15 :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α}, (|a| = a) = (0 ≤ a)
This theorem, from the `Mathlib.Algebra.Order.Group` library in Lean 4, states that for any arbitrary type `α` which is a `LinearOrderedAddCommGroup` - a group structure on addition with an order that is both linear and compatible with the addition operation, the absolute value of an element `a` from `α` is equal to `a` itself if and only if `a` is greater than or equal to zero. In mathematical terms, it states that for any `a` in `α`, `|a| = a` if and only if `a ≥ 0`.
More concisely: For any type `α` being a `LinearOrderedAddCommGroup`, the absolute value of an element `a` equals `a` if and only if `a` is non-negative.
|
abs_add
theorem abs_add : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a b : α), |a + b| ≤ |a| + |b|
This is the triangle inequality theorem for LinearOrderedAddCommGroups. For any type `α` that is a LinearOrderedAddCommGroup, and any two elements `a` and `b` of this type, the absolute value of the sum of `a` and `b` is less than or equal to the sum of the absolute values of `a` and `b`. In mathematical terms, this theorem states that \(|a + b| ≤ |a| + |b|\), a fundamental property of distances on the number line or in geometric spaces.
More concisely: For any element `a` and `b` in a LinearOrderedAddCommGroup `α`, the absolute difference of their sum and the sum of their absolute values is non-negative: `|a + b| ≤ |a| + |b|`.
|
abs_eq_self
theorem abs_eq_self : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α}, |a| = a ↔ 0 ≤ a
This theorem states that for any type `α` which is a linearly ordered additive commutative group, the absolute value of an element `a` of that type is equal to `a` if and only if `a` is greater than or equal to zero. The theorem is general and holds for any instance of a linearly ordered additive commutative group, which includes common types like integers and real numbers.
More concisely: For any linearly ordered additive commutative group type `α`, the absolute value of an element `a` equals `a` if and only if `a` is non-negative.
|
mabs_mul_le
theorem mabs_mul_le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : CommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a b : α),
mabs (a * b) ≤ mabs a * mabs b
The theorem `mabs_mul_le` states that for any type `α` that is a lattice and also a commutative group, and when multiplication is a covariant function on `α`, the absolute value of the product of two elements `a` and `b` from `α` is less than or equal to the product of their absolute values. This is known as the triangle inequality in the context of absolute values, which can be written in mathematical terms as `|a * b| ≤ |a| * |b|`.
More concisely: For any commutative group and lattice type `α` with covariant multiplication, the absolute value of their product is less than or equal to the product of their absolute values: `|a * b| ≤ |a| * |b|`.
|
abs_of_nonneg
theorem abs_of_nonneg :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 ≤ a → |a| = a
This theorem states that for any type `α` that is a lattice and an additive group, and for any element `a` of this type, if the addition operation for this type is covariant and the element `a` is nonnegative (i.e., `0 ≤ a`), then the absolute value of `a` is equal to `a` itself. In mathematical terms, if `α` is a type with the properties mentioned and `a` is an element of `α` such that `0 ≤ a`, then `|a| = a`.
More concisely: For any lattice and additive group type `α` with covariant addition, if `a` is a non-negative element of `α`, then `|a| = a`.
|
abs_of_nonpos
theorem abs_of_nonpos :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ 0 → |a| = -a
This theorem, `abs_of_nonpos`, states that for any type `α` that is a lattice and an additive group, and any element `a` of type `α`, if `a` is less than or equal to zero and the type `α` has a certain covariance property for addition and comparison, then the absolute value of `a` is equal to the negation of `a`. In mathematical terms, if `a ≤ 0`, then `|a| = -a`.
More concisely: For any lattice and additive group type `α`, if its additive and order structures have covariance property and `a` is an element of `α` with `a ≤ 0`, then `|a| = -a`.
|
abs_le
theorem abs_le : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b : α}, |a| ≤ b ↔ -b ≤ a ∧ a ≤ b
This theorem states that for any type `α` that is a linearly ordered additive commutative group, the absolute value of a member `a` of that type is less than or equal to another member `b` of that type if and only if `a` is greater than or equal to negative `b` and also less than or equal to `b`. This theorem essentially defines the mathematical property that the absolute value of a number is within a range centered at zero.
More concisely: For any linearly ordered additive commutative group type `α`, the absolute value `|a|` of `α` element `a` satisfies `-b ≤ a ≤ b` if and only if `|a| ≤ |b|`.
|
le_abs_self
theorem le_abs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), a ≤ |a|
This theorem states that for any type `α` which forms a lattice and is also an additive group, any element `a` of `α` is less than or equal to the absolute value of `a`. Here `|a|` denotes the absolute value of `a`.
More concisely: For any lattice and additive group type `α`, every element `a` in `α` satisfies `|a| ≥ a`.
|
neg_le_abs_self
theorem neg_le_abs_self : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), -a ≤ |a|
The theorem `neg_le_abs_self` states that for any element `a` from a type `α`, where `α` is a lattice and an additive group, the negation of `a` is less than or equal to the absolute value of `a`. This is essentially an alias of the `neg_le_abs` theorem. In mathematical terms, it expresses that for any `a` in a lattice and additive group, `-a ≤ |a|`.
More concisely: For any element `a` in a lattice and additive group `α`, `-a ≤ |a|`.
|
abs_cases
theorem abs_cases : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α), |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
This theorem states that for any element `a` of a linear ordered ring, two possible cases exist. In the first case, the absolute value of `a` is equal to `a` itself and `a` is greater than or equal to 0. In the second case, the absolute value of `a` is equal to the negation of `a` and `a` is less than 0. This theorem is useful in automating linear arithmetic in inequalities.
More concisely: For any element `a` in a linear ordered ring, the absolute value `|a|` satisfies `|a| = a` if `a` is non-negative, or `|a| = -a` if `a` is negative.
|
mabs_inv
theorem mabs_inv : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), mabs a⁻¹ = mabs a
The theorem `mabs_inv` states that for all types `α`, where `α` forms a lattice and a group, the absolute value function `mabs` is invariant under taking the inverse. This means that for any element `a` of the type `α`, the absolute value of the inverse of `a` is equal to the absolute value of `a`. In mathematical terms, this could be written as: for any `a` in the group, |a⁻¹| = |a|.
More concisely: For any element `a` in a group that forms a lattice, |a⁻¹| = |a|.
|
abs_eq_neg_self
theorem abs_eq_neg_self : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α}, |a| = -a ↔ a ≤ 0
This theorem states that for any type `α` that is a linear ordered additive commutative group, for an element `a` of type `α`, the absolute value of `a` is equal to the negative of `a` if and only if `a` is less than or equal to zero. Essentially, it ties the properties of absolute values and negation with the ordering of elements in the group, specifically for non-positive elements.
More concisely: For any linear ordered additive commutative group type `α` and element `a` of `α`, |a| = -a if and only if a ≤ 0.
|
max_sub_min_eq_abs
theorem max_sub_min_eq_abs :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : 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 = |b - a|
The theorem `max_sub_min_eq_abs` states that for any type `α` that is an additive group and a linear order, and that satisfies two specific covariant properties (where addition is increasing with respect to the order), the difference between the maximum and minimum of two elements `a` and `b` is equal to the absolute value of `b - a`. In more mathematical terms, for all `a` and `b` in `α`, we have `max(a, b) - min(a, b) = |b - a|`.
More concisely: For all additive groups and linearly ordered types `α` where addition is increasing with respect to the order, the difference between the maximum and minimum of any two elements `a` and `b` is equal to the absolute value of their difference: `|max(a, b) - min(a, b)| = |b - a|`.
|
abs_abs
theorem abs_abs :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), |(|a|)| = |a|
The theorem `abs_abs` states that for any type `α` that forms a lattice, an additive group, and satisfies two specific covariance conditions, the absolute value of the absolute value of any element `a` of type `α` is equal to the absolute value of `a`. In mathematical terms, it asserts that for any `a` in such a type `α`, ||a|| = |a|.
More concisely: For any type `α` that forms a lattice, an additive group, and satisfies the given covariance conditions, the absolute value of an element is equal to the absolute value of its absolute value, i.e., |||a||| = |a|.
|
abs_eq_zero
theorem abs_eq_zero :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], |a| = 0 ↔ a = 0
The theorem `abs_eq_zero` states that for any type `α` that is an additive group, a linear order, and possesses two specific covariance properties with respect to addition and order, the absolute value of an element `a` of type `α` equals zero if and only if `a` itself equals zero. In other words, within this mathematical structure, the only element whose absolute value is zero is the zero element itself.
More concisely: For any additive group, linear order type `α` with specific covariance properties, absolute value of `a` in `α` equals zero if and only if `a` is the zero element.
|
one_lt_mabs
theorem one_lt_mabs :
∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, 1 < mabs a ↔ a ≠ 1
The theorem `one_lt_mabs` states that for any type `α` which is a group and a linear order, and satisfies the covariant class property (that multiplication respects the order), the absolute value `mabs a` of an element `a` is greater than 1 if and only if `a` is not equal to 1. In other words, in such a structure, the absolute value of any element other than 1 is always greater than 1.
More concisely: For any group and linear order type `α` satisfying the covariant class property, `mabs a > 1 if and only if a ≠ 1`.
|
abs_neg
theorem abs_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), |(-a)| = |a|
This theorem, `abs_neg`, states that for any type `α` which is a Lattice and an AddGroup, the absolute value of the negation of any element `a` of type `α` is equal to the absolute value of `a`. In mathematical terms, the theorem expresses the property that |(-a)| = |a| for all `a` in this type `α`.
More concisely: For any type `α` being both a Lattice and an AddGroup, the absolute value of the negation of an element `a` equals the absolute value of `a`, i.e., |-a| = |a|.
|
abs_eq
theorem abs_eq : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b : α}, 0 ≤ b → (|a| = b ↔ a = b ∨ a = -b)
This theorem, `abs_eq`, states that for any type `α` which is a linearly ordered additive commutative group, and any two elements `a` and `b` of this type where `b` is non-negative, the absolute value of `a` being equal to `b` is equivalent to `a` being either `b` or the negative of `b`. In other words, if the absolute value of a number equals a non-negative number, then the original number must either be that non-negative number or its negative counterpart.
More concisely: For any linearly ordered additive commutative group type `α` and elements `a, b` of `α` with `b` non-negative, `|a| = b` if and only if `a = b` or `a = -b`.
|
abs_choice
theorem abs_choice : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] (x : α), |x| = x ∨ |x| = -x := by
sorry
This theorem, `abs_choice`, states that for any given type `α` which forms an additive group and has a linear order, the absolute value of any element `x` of this type is either equal to `x` itself or its negation. In other words, `|x| = x` or `|x| = -x` for any `x` in `α`. This is a typical property of absolute values in ordered additive groups.
More concisely: In an additive group with a linear order, the absolute value of any element is either the element itself or its negation.
|
abs_of_pos
theorem abs_of_pos :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α}
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < a → |a| = a
This theorem, `abs_of_pos`, states that for any type `α` which is a lattice, an add group, and satisfies the covariant class property, if `a` is an element of this type such that `a` is greater than zero, then the absolute value of `a` equals `a` itself. The purpose of this is to state a general property of absolute values: for any positive element, its absolute value simply equals the element itself. This theorem can be applied to any type that meets the constraints, making it a versatile and powerful statement in abstract algebraic environments.
More concisely: For any lattice, add group type `α` satisfying the covariant class property, if `a` is a positive element of `α`, then `|a| = a`.
|
neg_le_abs
theorem neg_le_abs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), -a ≤ |a|
This theorem states that for any type `α` which is a Lattice and an AddGroup, the negative of any element `a` of this type is less than or equal to the absolute value of `a`. In mathematical terms, we can say that for all `a` belonging to the type `α`, `-a ≤ |a|`.
More concisely: For any lattice and add group type `α`, the negation of each of its elements is less than or equal to its absolute value. (i.e., `-a ≤ |a|` for all `a` in `α`).
|
abs_sub_lt_iff
theorem abs_sub_lt_iff :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a b c : α}, |a - b| < c ↔ a - b < c ∧ b - a < c
This theorem states that for any type `α` that is a linearly ordered additive commutative group, and any three elements `a`, `b`, and `c` of this type, the absolute value of the difference between `a` and `b`, denoted `|a - b|`, is less than `c` if and only if `a - b` is less than `c` and `b - a` is less than `c`. In mathematical terms, this theorem is expressing the fact that |a - b| < c if and only if both a - b < c and b - a < c.
More concisely: For any linearly ordered additive commutative group type `α` and elements `a, b, c` of `α`, |a - b| < c if and only if both a - b and b - a are less than c.
|
neg_abs_le_self
theorem neg_abs_le_self :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), -|a| ≤ a
This theorem, named `neg_abs_le_self`, states that for any type `α` that is an additive group and also a linear order, with a covariant class such that addition implies an order relation, the negation of the absolute value of any element `a` of type `α` is less than or equal to `a`. In mathematical terms, for any `a` from a suitable type `α`, we have `-|a| ≤ a`.
More concisely: For any additive group and linear order type `α` where `a ≤ |a|` holds, we have `-|a| ≤ a`.
|
abs_sub_comm
theorem abs_sub_comm : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a b : α), |a - b| = |b - a| := by
sorry
This theorem states that for any type `α` that satisfies the properties of a lattice and an additive group, the absolute difference between any two elements `a` and `b` of `α` is the same regardless of the order in which `a` and `b` are subtracted. In other words, the absolute value of `a` subtracted from `b` is the same as the absolute value of `b` subtracted from `a`. This corresponds to the mathematical principle that the absolute value of the difference between two elements is unaffected by their order.
More concisely: For any lattice and additive group type `α`, the absolute difference between two elements `a` and `b` is commutative, that is, |a - b| = |b - a|.
|
abs_inf_sub_inf_le_abs
theorem abs_inf_sub_inf_le_abs :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
|a ⊓ c - b ⊓ c| ≤ |a - b|
This theorem, `abs_inf_sub_inf_le_abs`, states that for all types `α` that form a Lattice, and also form an Additive Commutative Group, with the additional property specified by the `CovariantClass` (the operation of adding two elements of the type preserves the order), the absolute value of the difference between the infimum of `a` and `c` and the infimum of `b` and `c` is less than or equal to the absolute value of the difference between `a` and `b`. In mathematical notation, we can say: for all `a`, `b`, and `c` in some type `α`, |∧(a, c) - ∧(b, c)| ≤ |a - b|. Here, ∧ denotes the infimum (greatest lower bound) of two elements.
More concisely: For all types `α` that are Lattices, Additive Commutative Groups with the Covariance property, the absolute value of the infimum difference between two elements `a` and `c`, and `b` and `c` is less than or equal to the absolute value of the difference between `a` and `b`. In mathematical notation: |∧(a, c) - ∧(b, c)| ≤ |a - b|.
|
Mathlib.Algebra.Order.Group.Abs._auxLemma.10
theorem Mathlib.Algebra.Order.Group.Abs._auxLemma.10 :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], (|a| = 0) = (a = 0)
The theorem `Mathlib.Algebra.Order.Group.Abs._auxLemma.10` states that for any type `α` which is an additive group and possesses a linear order and is covariant in both its regular addition operation and its swapped addition operation, the absolute value of an element `a` from `α` is equal to zero if and only if `a` itself is equal to zero. In other words, in this algebraic structure, an element's absolute value is zero exactly when the element is zero.
More concisely: For any additive group with a linear order covariant under swapped addition, the absolute value of an element is zero if and only if the element itself is zero.
|
abs_add_le
theorem abs_add_le :
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), |a + b| ≤ |a| + |b|
This theorem states that for any type `α` that possesses the structure of a lattice and an additive commutative group, and also satisfies the covariant property with respect to addition and order, the absolute value of the sum of any two elements `a` and `b` is always less than or equal to the sum of the absolute values of `a` and `b`. This is known as the triangle inequality in the context of absolute values.
More concisely: For any lattice and additive commutative group type `α` with covariant order and addition, the absolute value of `|a + b|` is less than or equal to `|a| + |b|` for all `a, b : α`. (Triangle inequality)
|