AbsoluteValue.eq_zero
theorem AbsoluteValue.eq_zero :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
abv x = 0 ↔ x = 0
This theorem is about the concept of absolute value in mathematics. Specifically, it states that for any absolute value function `abv` from a semiring `R` to an ordered semiring `S`, an element `x` in `R` will have an absolute value of zero if and only if `x` itself is zero. This mirrors the familiar property of absolute value in real numbers where the absolute value of a number is zero if and only if the number itself is zero.
More concisely: For any semiring homomorphism (absolute value function) `abv` from a semiring `R` to an ordered semiring `S`, `abv(x) = 0` if and only if `x = 0`.
|
AbsoluteValue.add_le
theorem AbsoluteValue.add_le :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x y : R), abv (x + y) ≤ abv x + abv y
This theorem states that for any types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and given an absolute value function `abv` from `R` to `S`, the absolute value of the sum of two elements `x` and `y` in `R` is less than or equal to the sum of the absolute values of `x` and `y`. This is a formal statement of the triangle inequality for absolute values in the context of semirings.
More concisely: For any semirings R and S with an ordered semiring structure on S, and an absolute value function from R to S, |x + y| ≤ |x| + |y| holds for all x, y in R. (Triangle inequality for absolute values in semirings)
|
AbsoluteValue.add_le'
theorem AbsoluteValue.add_le' :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S)
(x y : R), self.toFun (x + y) ≤ self.toFun x + self.toFun y
The theorem `AbsoluteValue.add_le'` states that for any two elements `x` and `y` of a semiring `R`, the absolute value of their sum is less than or equal to the sum of their absolute values. This property, known as the triangle inequality, holds for absolute values defined on semirings `R` with an ordered semiring `S`. The absolute value is a function from `R` to `S`.
More concisely: For any semiring `R` with an ordered semiring `S` and absolute value function `|.|` from `R` to `S`, |x + y| ≤ |x| + |y| for all x, y in R. (This is the triangle inequality for absolute values.)
|
AbsoluteValue.ne_zero_iff
theorem AbsoluteValue.ne_zero_iff :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
abv x ≠ 0 ↔ x ≠ 0
This theorem states that for any types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, the absolute value function `abv` from `R` to `S` applied to a value `x` from `R` is not equal to zero if and only if `x` is not equal to zero. In other words, the absolute value of a number is non-zero exactly when the number itself is non-zero.
More concisely: For all semirings R and ordered semirings S, the absolute value function from R to S satisfies |x| ≠ 0 if and only if x ≠ 0.
|
AbsoluteValue.pos
theorem AbsoluteValue.pos :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
x ≠ 0 → 0 < abv x
This theorem states that for any types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and for any absolute value function `abv` from `R` to `S`, if `x` is a non-zero element of `R`, then the absolute value of `x` (i.e., `abv x`) is greater than zero. It essentially asserts the well-known mathematical property that the absolute value of a non-zero number is always positive.
More concisely: For any semiring `R`, ordered semiring `S`, and absolute value function `abv` from `R` to `S`, if `x` is a non-zero element of `R`, then `abv x > 0`.
|
AbsoluteValue.map_mul
theorem AbsoluteValue.map_mul :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S)
(x y : R), abv (x * y) = abv x * abv y
This theorem states that for any two types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and for any absolute value function `abv` from `R` to `S`, the absolute value of the product of two elements `x` and `y` from `R` is equal to the product of their absolute values. In other words, if you multiply two numbers together and then take the absolute value, you get the same result as if you took the absolute values first and then multiplied. This property is represented symbolically as `abv (x * y) = abv x * abv y`.
More concisely: For any semiring `R`, ordered semiring `S`, and absolute value function `abv` from `R` to `S`, `abv (x * y) = abv x * abv y` for all `x, y` in `R`.
|
AbsoluteValue.nonneg'
theorem AbsoluteValue.nonneg' :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
0 ≤ self.toFun x
This theorem asserts that the absolute value of any number is nonnegative. More precisely, it applies to any number `x` of type `R` in a semiring, and the absolute value function `self` that maps `R` to `S`, where `S` is an ordered semiring. The result of applying `self` to `x`, i.e., the absolute value of `x`, is always greater than or equal to zero.
More concisely: For all `x` in a semiring `R` with an order relation in an ordered semiring `S`, |x| ≥ 0, where |.| denotes the absolute value function.
|
IsAbsoluteValue.abv_add
theorem IsAbsoluteValue.abv_add :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] (abv : R → S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x + y) ≤ abv x + abv y
This theorem states that for any ordered semiring `S` and any semiring `R`, given an absolute value function `abv` from `R` to `S`, and any elements `x` and `y` from `R`, the absolute value of the sum of `x` and `y` is less than or equal to the sum of the absolute values of `x` and `y`. This is a generalization of the triangle inequality in the context of absolute values in semirings.
More concisely: For any ordered semirings S and semiring R, and absolute value function abv from R to S, |x + y| ≤ |x| + |y| holds for all x, y in R.
|
IsAbsoluteValue.abv_zero
theorem IsAbsoluteValue.abv_zero :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] (abv : R → S)
[inst_2 : IsAbsoluteValue abv], abv 0 = 0
This theorem states that for any ordered semiring `S` and any semiring `R`, given a function `abv` from `R` to `S` that represents an absolute value, the absolute value of zero is zero. This is a basic property of absolute values in mathematics, and this theorem captures that fact in the context of abstract algebra using semirings.
More concisely: For any ordered semirings S and semiring R with an absolute value function abv from R to S, abv(0) = 0.
|
AbsoluteValue.nonneg
theorem AbsoluteValue.nonneg :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (x : R),
0 ≤ abv x
This theorem states that for any types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and any absolute value function `abv` from `R` to `S`, the absolute value of any element `x` of `R` is always nonnegative. In mathematical terms, it asserts that for all `x` in `R`, `0 ≤ |x|`.
More concisely: For any semiring `R`, ordered semiring `S`, and absolute value function `abv` from `R` to `S`, |x| ≥ 0 for all x in R.
|
AbsoluteValue.eq_zero'
theorem AbsoluteValue.eq_zero' :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (self : AbsoluteValue R S) (x : R),
self.toFun x = 0 ↔ x = 0
This theorem states that for any types `R` and `S` where `R` is a semiring and `S` is an ordered semiring, and for any absolute value function from `R` to `S` (represented by `self.toFun`), a value `x` from `R` maps to zero if and only if `x` is zero. In other words, in this context, the only number which has an absolute value of zero is zero itself.
More concisely: For any semiring `R`, ordered semiring `S`, and absolute value function `f : R → S` from `R` to `S`, `f x = 0` if and only if `x = 0`.
|
AbsoluteValue.ext
theorem AbsoluteValue.ext :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] ⦃f g : AbsoluteValue R S⦄,
(∀ (x : R), f x = g x) → f = g
This theorem, `AbsoluteValue.ext`, states that for any two types `R` and `S`, with `R` being a semiring and `S` a ordered semiring, if you have two absolute value functions `f` and `g` from `R` to `S`, and for every value in `R` both `f` and `g` give the same result, then `f` and `g` must be the same function. Essentially, this theorem ensures that an absolute value function is uniquely determined by its action on all elements of `R`.
More concisely: If `R` is a semiring and `S` an ordered semiring, and `f` and `g` are absolute value functions from `R` to `S` such that `f(x) = g(x)` for all `x` in `R`, then `f` and `g` are equal functions.
|
IsAbsoluteValue.abv_mul
theorem IsAbsoluteValue.abv_mul :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] (abv : R → S)
[inst_2 : IsAbsoluteValue abv] (x y : R), abv (x * y) = abv x * abv y
This theorem states that for any ordered semiring `S` and any semiring `R`, given a function `abv : R → S` which is an absolute value function, the absolute value of the product of `x` and `y` (both elements of `R`) is equal to the product of the absolute values of `x` and `y`. That is, if `abv` is an absolute value function, then `abv (x * y) = abv x * abv y` for any `x` and `y` in `R`.
More concisely: For any semiring `R` and absolute value function `abv : R → ℝ` from `R` to the real numbers, `abv (x * y) = abv x * abv y` for all `x, y` in `R`.
|
AbsoluteValue.ne_zero
theorem AbsoluteValue.ne_zero :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
x ≠ 0 → abv x ≠ 0
This theorem states that for any given types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and for any absolute value function `abv` from `R` to `S`, if a value `x` from `R` is not equal to zero, then the absolute value of `x` (i.e., `abv x`) is also not equal to zero. This is a generalization of the familiar property of absolute values from real numbers, where the absolute value of a non-zero number is always non-zero.
More concisely: If `abv` is an absolute value function from the semiring `R` to the ordered semiring `S`, then `abv (xs : R) ≠ 0` whenever `xs ≠ 0`.
|
IsAbsoluteValue.abv_mul'
theorem IsAbsoluteValue.abv_mul' :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] {f : R → S}
[self : IsAbsoluteValue f] (x y : R), f (x * y) = f x * f y
This theorem states that the function `f`, which is an absolute value function on a semiring `R` with values in an ordered semiring `S`, has the property that it is multiplicative. In other words, for any two elements `x` and `y` in `R`, the absolute value of their product is equal to the product of their absolute values, i.e., `f(x * y) = f(x) * f(y)`. This is a well-known property of absolute values in the context of algebra.
More concisely: The absolute value function on a semiring is multiplicative, that is, |x * y| = |x| * |y| for all x, y in the semiring.
|
AbsoluteValue.map_sub
theorem AbsoluteValue.map_sub :
∀ {R : Type u_3} {S : Type u_4} [inst : OrderedCommRing S] [inst_1 : Ring R] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a b : R), abv (a - b) = abv (b - a)
This theorem states that for any two elements `a` and `b` from a ring `R` and an absolute value function `abv` mapping from this ring `R` to an ordered commutative ring `S` that has no zero divisors, the absolute value of the difference `a - b` is equal to the absolute value of the difference `b - a`. In mathematical terms, this can be written as |a - b| = |b - a|. This is a fundamental property of absolute values, reflecting the idea that the absolute value of a difference is insensitive to the order of subtraction.
More concisely: For any ring `R` with absolute value function `abv` mapping from `R` to an ordered commutative ring `S` with no zero divisors, |a - b| = |b - a| for all `a, b` in `R`.
|
IsAbsoluteValue.abv_nonneg'
theorem IsAbsoluteValue.abv_nonneg' :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] {f : R → S}
[self : IsAbsoluteValue f] (x : R), 0 ≤ f x
This theorem states that the absolute value of any real number is always nonnegative. In more detail, for any types `S` and `R`, where `S` is an ordered semiring and `R` is a semiring, and for any function `f` that acts as an absolute value (as defined by `IsAbsoluteValue f`), the value of `f(x)` is always greater than or equal to zero for any `x` in `R`.
More concisely: For any semiring `R` and absolute value function `f` on `R`, `|x| ≥ 0` for all `x` in `R`.
|
IsAbsoluteValue.abv_eq_zero'
theorem IsAbsoluteValue.abv_eq_zero' :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] {f : R → S}
[self : IsAbsoluteValue f] {x : R}, f x = 0 ↔ x = 0
This theorem states that for any ordered semiring `S`, any semiring `R`, and any function `f` from `R` to `S` that is an absolute value, the absolute value of `x` (i.e., `f(x)`) is equal to zero if and only if `x` itself is zero. In other words, the only input for which the absolute value function gives zero is zero itself. This is a property characteristic of absolute value functions on semirings.
More concisely: For any ordered semirings S and semiring R, and absolute value function f from R to S, f(x) = 0 if and only if x = 0.
|
IsAbsoluteValue.abv_add'
theorem IsAbsoluteValue.abv_add' :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] {f : R → S}
[self : IsAbsoluteValue f] (x y : R), f (x + y) ≤ f x + f y
This theorem states that for any ordered semiring `S` and any semiring `R`, if `f` is a function from `R` to `S` and `f` is an absolute value function, then for any elements `x` and `y` in `R`, the absolute value of their sum is less than or equal to the sum of their absolute values. This is a formal statement of the triangle inequality in the context of semirings.
More concisely: For any ordered semirings S and semiring R, and absolute value function f : R -> S, |f(x + y)| <= |f(x)| + |f(y)| holds for all x, y in R.
|
IsAbsoluteValue.abv_nonneg
theorem IsAbsoluteValue.abv_nonneg :
∀ {S : Type u_5} [inst : OrderedSemiring S] {R : Type u_6} [inst_1 : Semiring R] (abv : R → S)
[inst_2 : IsAbsoluteValue abv] (x : R), 0 ≤ abv x
The theorem `IsAbsoluteValue.abv_nonneg` states that for any ordered semiring `S`, semiring `R`, and any function `abv` from `R` to `S` that is an absolute value, the absolute value of any element `x` from `R` is always nonnegative. In other words, the absolute value of a number, under these mathematical conditions, can never be less than zero.
More concisely: For any ordered semiring (S, ≤) and semiring (R, +, *) with an absolute value function abv : R -> S, ∀ x : R, abv x ≥ 0.
|
AbsoluteValue.sub_le
theorem AbsoluteValue.sub_le :
∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) (a b c : R),
abv (a - c) ≤ abv (a - b) + abv (b - c)
This theorem states that for any types `R` and `S`, where `R` is a ring and `S` is an ordered semiring, and any absolute value function `abv` from `R` to `S`, and for any elements `a`, `b`, and `c` in `R`, the absolute value of `(a - c)` is less than or equal to the sum of the absolute values of `(a - b)` and `(b - c)`. This is a formal representation of the triangle inequality in the context of absolute values in arbitrary rings.
More concisely: For any rings R and ordered semirings S, absolute value functions abv from R to S, and elements a, b, c in R, |a - c| ≤ |a - b| + |b - c| (triangle inequality for absolute values).
|
AbsoluteValue.pos_iff
theorem AbsoluteValue.pos_iff :
∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : OrderedSemiring S] (abv : AbsoluteValue R S) {x : R},
0 < abv x ↔ x ≠ 0
This theorem states that for any types `R` and `S`, where `R` is a semiring and `S` is an ordered semiring, and for any absolute value function `abv` from `R` to `S`, the absolute value of `x` (a member of `R`) is positive if and only if `x` is not zero. In more mathematical terms, this is stating that the absolute value of `x`, denoted as `|x|`, is greater than 0 if and only if `x ≠ 0`.
More concisely: For any semiring `R`, ordered semiring `S`, and absolute value function `abv` from `R` to `S`, |x| > 0 if and only if x ≠ 0.
|
AbsoluteValue.abs_abv_sub_le_abv_sub
theorem AbsoluteValue.abs_abv_sub_le_abv_sub :
∀ {R : Type u_5} {S : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S)
(a b : R), |abv a - abv b| ≤ abv (a - b)
This theorem states that for any types `R` and `S`, where `R` is a ring and `S` is a linear ordered commutative ring, and for any absolute value function `abv` from `R` to `S`, and any elements `a` and `b` of `R`, the absolute value of the difference of `abv a` and `abv b` is less than or equal to the absolute value of the difference of `a` and `b`. This is essentially a kind of triangle inequality for the absolute value function `abv`.
More concisely: For any ring `R`, commutative ring `S` with order, and absolute value function `abv` from `R` to `S`, |abv(a) - abv(b)| ≤ |a - b| for all elements `a, b` in `R`.
|
AbsoluteValue.map_neg
theorem AbsoluteValue.map_neg :
∀ {R : Type u_3} {S : Type u_4} [inst : OrderedCommRing S] [inst_1 : Ring R] (abv : AbsoluteValue R S)
[inst_2 : NoZeroDivisors S] (a : R), abv (-a) = abv a
This theorem states that for any given types `R` and `S`, where `S` is an ordered commutative ring and `R` is a ring, and any absolute value `abv` from `R` to `S`, if `S` has no zero divisors, then the absolute value of the negation of any element `a` from `R` is equal to the absolute value of `a`. In mathematical terms, this means that |−a| = |a| for any `a` in `R`, which is a standard property of absolute values in mathematics.
More concisely: Given rings `R` and `S` with `S` an ordered commutative ring without zero divisors, and an absolute value `abv` from `R` to `S`, then for all `a` in `R`, we have |−`a`| = |`a`|.
|