iUnion_Ioc_add_zsmul
theorem iUnion_Ioc_add_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [inst_1 : Archimedean α] {p : α},
0 < p → ∀ (a : α), ⋃ n, Set.Ioc (a + n • p) (a + (n + 1) • p) = Set.univ
The theorem `iUnion_Ioc_add_zsmul` states that for any type `α` that is a linear ordered additive commutative group and Archimedean, and for any positive element `p` of `α`, and any element `a` of `α`, the union over all integers `n` of the left-open right-closed intervals from `a + np` to `a + (n+1)p` equals the universal set. This means that every element of `α` is contained in one of these intervals. In other words, we can cover the entire set `α` by shifting the interval `(a, a+p]` by integer multiples of `p`.
More concisely: For any Archimedean additive commutative group `α` with a positive element `p`, every element of `α` lies in some left-open right-closed interval `[a + np, a + (n+1)p)` for some integer `n`.
|
AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod
theorem AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b : α},
¬a ≡ b [PMOD p] ↔ toIcoMod hp a b = toIocMod hp a b
The theorem `AddCommGroup.not_modEq_iff_toIcoMod_eq_toIocMod` states that for any type `α` that is a linear ordered additive commutative group and an Archimedean field, and for any positive real number `p`, and any two real numbers `a` and `b`, `a` is not congruent to `b` modulo `p` if and only if the reduction of `b` to the interval `[a, a + p)` (`toIcoMod`) is equal to the reduction of `b` to the interval `(a, a + p]` (`toIocMod`).
More concisely: For any Archimedean additive commutative group `α`, real numbers `p`, `a`, and `b`, `a` is not congruent to `b` modulo `p` if and only if `toIcoMod p a b` equals `toIocMod p a b`.
|
AddCommGroup.ModEq.toIcoMod_eq_right
theorem AddCommGroup.ModEq.toIcoMod_eq_right :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b : α},
a ≡ b [PMOD p] → toIocMod hp a b = a + p
This theorem, named `AddCommGroup.ModEq.toIcoMod_eq_right`, states that for any type `α` that is a linearly ordered additive commutative group and also satisfies the Archimedean property, and for any positive element `p` of `α`, given any two elements `a` and `b` of `α`, if `a` is congruent to `b` modulo `p` (denoted as `a ≡ b [PMOD p]`), then the result of applying the function `toIocMod` with `p`, `a`, and `b` as inputs is equal to `a + p`. The function `toIocMod` reduces `b` to the half-open interval `(a, a + p]`.
More concisely: For any Archimedean additive commutative group `α` and positive element `p` of `α`, if `a ≡ b [PMOD p]`, then `toIcoMod p a b = a + p`.
|
sub_toIocDiv_zsmul_mem_Ioc
theorem sub_toIocDiv_zsmul_mem_Ioc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
b - toIocDiv hp a b • p ∈ Set.Ioc a (a + p)
The theorem `sub_toIocDiv_zsmul_mem_Ioc` asserts that for any type `α` that is a linear ordered additive commutative group and can be embedded in the real numbers (Archimedean property), and for any positive value `p` of type `α`, and any values `a` and `b` of type `α`, the result of subtracting the product of `p` and the unique integer given by the function `toIocDiv` applied to `hp`, `a` and `b` from `b`, lies in the interval `(a, a + p]`. Here, the interval `(a, a + p]` is a set of all elements `x` of type `α` such that `a < x <= a + p`.
More concisely: For any Archimedean linear ordered additive commutative group type `α`, positive value `p` of type `α`, and values `a` and `b` of type `α` with `a < b`, the result of subtracting `p * (toIocDiv p (b - a))` from `b` lies in the interval `(a, a + p]`.
|
toIocDiv_eq_of_sub_zsmul_mem_Ioc
theorem toIocDiv_eq_of_sub_zsmul_mem_Ioc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : ℤ},
b - n • p ∈ Set.Ioc a (a + p) → toIocDiv hp a b = n
This theorem, `toIocDiv_eq_of_sub_zsmul_mem_Ioc`, states that for any type `α` that forms a linearly ordered additive commutative group with the Archimedean property, given a positive element `p`, and any two elements `a` and `b` of the group and any integer `n`, if the result of subtracting `n` times `p` from `b` belongs to the left-open right-closed interval from `a` to `a + p`, then the unique integer associated with `b` such that this multiple of `p`, subtracted from `b`, is in the same left-open right-closed interval- as defined by the function `toIocDiv`, is equal to `n`.
More concisely: For any Archimedean additive commutative group type `α` with positive element `p`, if `n` is an integer such that `n * p` belongs to the left-open right-closed interval from `a` to `a + p`, then `toIocDiv a (b - n * p) = n`.
|
toIocMod_add_zsmul
theorem toIocMod_add_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ℤ),
toIocMod hp a (b + m • p) = toIocMod hp a b
The theorem `toIocMod_add_zsmul` states that for any type `α` that is a linearly ordered additive commutative group and satisfies the Archimedean property, given a positive element `p`, two elements `a` and `b` of `α`, and an integer `m`, the operation `toIocMod` applied to `a` and `(b + m • p)` is equal to `toIocMod` applied to `a` and `b`. Here, `toIocMod` is a function that reduces `b` to the interval `(a, a + p)`, and `m • p` represents the multiplication of the integer `m` with the element `p`.
More concisely: For any Archimedean, additively commutative group `α` with a positive element `p`, and integers `m` and `a, b` in `α`, `toIocMod a (b + m*p) = toIocMod a b`.
|
AddCommGroup.ModEq.toIcoMod_eq_toIcoMod
theorem AddCommGroup.ModEq.toIcoMod_eq_toIcoMod :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b c : α},
a ≡ b [PMOD p] → toIcoMod hp c a = toIcoMod hp c b
This theorem, named `AddCommGroup.ModEq.toIcoMod_eq_toIcoMod`, states that for any type `α` that is a linearly ordered additive commutative group and satisfies the Archimedean property, if `a` and `b` are congruent modulo `p` (where `p` is positive), then reducing `a` and `b` to the interval `[c, c + p)` using the `toIcoMod` function yields the same result. Essentially, if `a` and `b` fall within the same cycle with respect to `c`, then they are congruent modulo `p`.
More concisely: For any linearly ordered additive commutative Archimedean group `α` and positive `p`, if `a` and `b` are congruent modulo `p`, then `toIcoMod a c p` equals `toIcoMod b c p`.
|
toIcoDiv_add_zsmul
theorem toIcoDiv_add_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ℤ),
toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + m
The theorem `toIcoDiv_add_zsmul` states that for any type `α` that has a structure of a linearly ordered additive commutative group and satisfies the Archimedean property, for any positive element `p` of `α`, and for any other two elements `a` and `b` of `α` and an integer `m`, the unique integer `toIcoDiv hp a (b + m • p)` obtained by subtracting `m` times `p` added to `b` from the multiple of `p` that lies in the interval from `a` to `a + p`, is equal to the unique integer `toIcoDiv hp a b` obtained by subtracting `b` from the multiple of `p` that lies in the interval from `a` to `a + p`, plus `m`. This essentially captures the translational invariance property of the division operation in the context of additive groups.
More concisely: For any type `α` with a linearly ordered additive commutative group structure and the Archimedean property, the integer obtained by dividing `b + m • p` by `p` in the interval `[a, a + p]` is equal to the integer obtained by dividing `a` by `p` and adding `m`, where `p` is positive, `a` and `b` are in `α`, and `m` is an integer.
|
toIocDiv_sub_eq_toIocDiv_add
theorem toIocDiv_sub_eq_toIocDiv_add :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b c : α),
toIocDiv hp a (b - c) = toIocDiv hp (a + c) b
This theorem states that for any type `α` that forms a linearly ordered additive commutative group and has the Archimedean property, and for any positive element `p` of `α`, and any three elements `a`, `b`, and `c` of `α`, the unique integer obtained by subtracting `c` from `b` and then applying the `toIocDiv` operation with parameters `hp` and `a`, is the same as the unique integer obtained by adding `c` to `a` and then applying the `toIocDiv` operation with parameters `hp` and `b`. In other words, the process of subtracting `c` from `b` before the `toIocDiv` operation is interchangeable with the process of adding `c` to `a` before the `toIocDiv` operation.
More concisely: For any linearly ordered additive commutative group `α` with the Archimedean property and positive element `p`, the result of subtracting `c` from `b` and then taking the integer quotient with `p` is equal to the result of adding `c` to `a` and then taking the integer quotient with `p`, for all `a, b, c` in `α`.
|
toIcoMod_add_zsmul
theorem toIcoMod_add_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ℤ),
toIcoMod hp a (b + m • p) = toIcoMod hp a b
This theorem states that for any type `α` that is a linear ordered add commutative group and also an Archimedean field, given a positive element `p`, two elements `a` and `b` of the same type, and an integer `m`, the function `toIcoMod` applied to `a` and `(b + m * p)` is the same as the function `toIcoMod` applied to `a` and `b`. In other words, adding an integer multiple of `p` to `b` does not change the value returned by the `toIcoMod` function. This essentially illustrates the periodicity property in the interval `[a, a+p)`.
More concisely: For any linear ordered add commutative group and Archimedean field `α`, and positive element `p` of `α`, for all integers `m` and elements `a, b` of `α`, `toIcoMod a (b + m * p) = toIcoMod a b`.
|
AddCommGroup.ModEq.toIcoMod_eq_left
theorem AddCommGroup.ModEq.toIcoMod_eq_left :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b : α},
a ≡ b [PMOD p] → toIcoMod hp a b = a
This theorem, named `AddCommGroup.ModEq.toIcoMod_eq_left`, states that for any type `α` which is a linearly ordered additive commutative group and Archimedean, given a positive element `p` and any two elements `a` and `b` of `α`, if `a` is congruent to `b` modulo `p`, then reducing `b` to the interval `Ico a (a + p)` using the function `toIcoMod` results in the value `a`. In mathematical terms, if `a ≡ b (mod p)`, then `toIcoMod hp a b = a`.
More concisely: For any Archimedean additive commutative group `α` and positive element `p`, if `a` is congruent to `b` modulo `p`, then `toIcoMod p a b = a`.
|
toIcoDiv_eq_of_sub_zsmul_mem_Ico
theorem toIcoDiv_eq_of_sub_zsmul_mem_Ico :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b : α} {n : ℤ},
b - n • p ∈ Set.Ico a (a + p) → toIcoDiv hp a b = n
This theorem states that for any Archimedean linearly ordered additive commutative group `α` and for any positive `p` in `α`, if the number obtained by subtracting `n` times `p` from `b` lies in the left-closed right-open interval from `a` to `a + p`, then the unique integer which when multiplied by `p` and subtracted from `b` lies in the same interval `a` to `a + p`, is `n`. Here, `n` is an integer and `a`, `b`, and `p` are elements of `α`.
More concisely: For any Archimedean linearly ordered additive commutative group `α`, and positive `p` in `α`, if `b - np` lies in the interval `[a, a + p)`, then `n` is the unique integer such that `b - np` belongs to `[a, a + p)`.
|
toIocDiv_add_zsmul
theorem toIocDiv_add_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α) (m : ℤ),
toIocDiv hp a (b + m • p) = toIocDiv hp a b + m
The theorem `toIocDiv_add_zsmul` states that for any type `α` that is a linear ordered additive commutative group and Archimedean, for any positive `p` of type `α`, and for any `a`, `b` of type `α` and integer `m`, the unique integer obtained by applying the `toIocDiv` function to the input `a` and `b + m * p` is equal to the sum of the unique integer obtained by applying the `toIocDiv` function to `a` and `b`, and `m`. In other words, adding `m` multiples of `p` to `b` before applying the `toIocDiv` function is the same as adding `m` to the result of applying the `toIocDiv` function to `a` and `b` without `m * p`.
More concisely: For any Archimedean linear ordered additive commutative group type `α` with positive element `p`, and integers `m` and `a`, `b` of type `α`, the result of applying `toIocDiv` to `a` and `b + m * p` is equal to the sum of the result of applying `toIocDiv` to `a` and `b`, and the integer `m`.
|
toIocMod_mem_Ioc
theorem toIocMod_mem_Ioc :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
toIocMod hp a b ∈ Set.Ioc a (a + p)
This theorem states that for any type `α` which forms a Linear Ordered Additive Commutative Group and is Archimedean, and for any positive `p`, given any `a` and `b` of type `α`, the result of the function `toIocMod` applied to `hp` (which is the proof that `p` is positive), `a`, and `b` will always be an element of the set `Set.Ioc` from `a` to `a + p`. In mathematical terms, you could say that the function `toIocMod` maps any `b` into the half-open interval `(a, a + p]`.
More concisely: For any Archimedean Linear Ordered Additive Commutative Group `α` and positive `p` in `α`, the image of `b` under the `toIocMod` function lies in the half-open interval `(a, a + p]` for all `a` in `α`.
|
toIocMod_eq_iff
theorem toIocMod_eq_iff :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b c : α},
toIocMod hp a b = c ↔ c ∈ Set.Ioc a (a + p) ∧ ∃ z, b = c + z • p
The theorem `toIocMod_eq_iff` states that for any type `α` that is a linear ordered additive commutative group and an Archimedean field, given a positive value `p`, and three elements `a`, `b`, and `c` from `α`, the result `c` of the function `toIocMod` applied with `hp`, `a` and `b` is equal to `c` if and only if `c` belongs to the left-open right-closed interval from `a` to `a + p` (`Set.Ioc a (a + p)`) and there exists a scalar `z` such that `b` equals `c` plus `z` times `p`.
More concisely: For any Archimedean linear ordered additive commutative group `α` and positive `p` in `α`, the element `c` belongs to the interval `Set.Ioc a (a + p)` and is of the form `b + k * p` for some scalar `k` if and only if `toIocMod p a b = c`.
|
Mathlib.Algebra.Order.ToIntervalMod._auxLemma.17
theorem Mathlib.Algebra.Order.ToIntervalMod._auxLemma.17 :
∀ {G : Type u_1} [inst : AddSemigroup G] (a b c : G), a + (b + c) = a + b + c
This theorem, `Mathlib.Algebra.Order.ToIntervalMod._auxLemma.17`, establishes that for any type `G` that has an `AddSemigroup` instance, the addition operation (`+`) is associative. In other words, given any three elements `a`, `b`, and `c` of type `G`, the sum of `a` and the sum of `b` and `c` (`a + (b + c)`) is equal to the sum of `a` and `b` added to `c` (`a + b + c`).
More concisely: For any type `G` with an `AddSemigroup` structure, the associativity of addition holds: `a + (b + c) = (a + b) + c` for all `a, b, c` in `G`.
|
AddCommGroup.tfae_modEq
theorem AddCommGroup.tfae_modEq :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
[a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b,
toIcoMod hp a b + p = toIocMod hp a b].TFAE
The theorem `AddCommGroup.tfae_modEq` states that for any type `α` which forms a linear ordered additive commutative group and has the Archimedean property, and given any `p` in `α` such that `p` is greater than 0, and any `a` and `b` in `α`, the following propositions are equivalent:
1. `a` is congruent to `b` modulo `p`.
2. For any integer `z`, the difference `b - z*p` is not in the open interval `(a, a + p)`.
3. The result of reducing `b` to the left-closed right-open interval `[a, a + p)` by subtracting an appropriate multiple of `p` is not equal to the result of reducing `b` to the open interval `(a, a + p]` by subtracting an appropriate multiple of `p`.
4. The result of reducing `b` to the left-closed right-open interval `[a, a + p)` by subtracting an appropriate multiple of `p` plus `p` is equal to the result of reducing `b` to the open interval `(a, a + p]` by subtracting an appropriate multiple of `p`.
More concisely: For any element `p` in a linearly ordered, additively commutative group `α` with the Archimedean property, and for all `a`, `b` in `α`, the statements "`a` is congruent to `b` modulo `p`" are equivalent to "the difference `b - p*z` is not in the open interval `(a, a + p)` for any integer `z`."
|
toIcoMod_mem_Ico
theorem toIcoMod_mem_Ico :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
toIcoMod hp a b ∈ Set.Ico a (a + p)
The theorem `toIcoMod_mem_Ico` states that for all types `α` that are instances of a linear ordered additive commutative group and an Archimedean field, and for any positive `p` (`0 < p`) and any two values `a` and `b` of type `α`, the result of the function `toIcoMod` applied to `hp` (the proof that `p` is positive), `a`, and `b` belongs to the set of values `x` which satisfy the condition `a ≤ x < a + p`. In other words, the theorem confirms that the `toIcoMod` function always maps `b` to a value that lies in the half-open interval from `a` (inclusive) to `a + p` (exclusive).
More concisely: For all Archimedean additive commutative groups α and positive p, the result of the `toIcoMod` function applied to p and any a in α is an element of the half-open interval [a, a + p).
|
toIcoMod_inj
theorem toIcoMod_inj :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b c : α},
toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]
This theorem states that for any type `α` which forms a linearly ordered additive commutative group and satisfies the Archimedean property, given a positive element `p` of that type, if two elements `a` and `b` are reduced to the same interval `Ico c (c + p)` (in other words, if `a` and `b` fall within the same cycle with respect to `c`), then `a` and `b` are congruent modulo `p`. This is expressed mathematically as `a ≡ b (mod p)`.
More concisely: For any linearly ordered additive commutative group `α` satisfying the Archimedean property, if `p` is a positive element and `a` and `b` lie in the same interval `Ico c (c + p)`, then `a` is congruent to `b` modulo `p`, denoted `a ≡ b (mod p)`.
|
toIcoMod_add_toIcoDiv_zsmul
theorem toIcoMod_add_toIcoDiv_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
toIcoMod hp a b + toIcoDiv hp a b • p = b
This theorem states that for any type `α` that forms an Archimedean linear ordered additive commutative group, and for any real number `p` that is greater than zero, and for any real numbers `a` and `b`, the value obtained by adding `p` multiplied by the unique integer from function `toIcoDiv` to the result of function `toIcoMod` is equal to `b`. This essentially transforms `b` into an element of the interval [a, a+p) and then adds back the integer multiple of `p` that was subtracted, thus recovering the original value `b`.
More concisely: For any Archimedean linear ordered additive commutative group type `α`, real number `p > 0`, and real numbers `a` and `b`, `b = a + p * (toIcoMod int p b + toIcoDiv int p a)`, where `toIcoMod` and `toIcoDiv` are the functions from Lean 4 used to convert real numbers to integers in the interval modulo and division operations, respectively.
|
toIcoDiv_sub_eq_toIcoDiv_add
theorem toIcoDiv_sub_eq_toIcoDiv_add :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b c : α),
toIcoDiv hp a (b - c) = toIcoDiv hp (a + c) b
This theorem states that for any type `α` that is an instance of the `LinearOrderedAddCommGroup` and `Archimedean`, and for any positive `p`, `a`, `b`, and `c` of type `α`, the unique integer obtained by subtracting `c` from `b` and then using the `toIcoDiv` function is equal to the unique integer obtained by adding `c` to `a` and then using the `toIcoDiv` function on `b`. In other words, the operation of subtracting `c` from `b` before applying `toIcoDiv` is the same as adding `c` to `a` before applying `toIcoDiv` on `b`.
More concisely: For any `α` instance of `LinearOrderedAddCommGroup` and `Archimedean`, the result of `toIcoDiv (b - c)` is equal to `toIcoDiv (a + c)` for any `p > 0` and `a, b, c : α`.
|
toIocMod_add_toIocDiv_zsmul
theorem toIocMod_add_toIocDiv_zsmul :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
toIocMod hp a b + toIocDiv hp a b • p = b
The theorem `toIocMod_add_toIocDiv_zsmul` states that for any type `α` that is a linearly ordered additive commutative group with the Archimedean property, and for any positive `p` in `α` and any elements `a` and `b` in `α`, the sum of the result of reducing `b` to the interval `(a, a + p)` and the integer multiple of `p` that is the unique integer such that this multiple of `p`, subtracted from `b`, is in the interval `(a, a + p)` is equal to `b`. In other words, `b` can be decomposed into a part that lies in the interval `(a, a + p)` (given by `toIocMod hp a b`) and the rest, which is an integer multiple of `p` (given by `toIocDiv hp a b • p`).
More concisely: For any Archimedean linearly ordered additive commutative group `α` and positive `p` in `α`, for all `a, b` in `α`, there exists an integer `n` such that `b = toIocMod p a b + n*p`, where `toIocMod` is the operation of reducing an element to the interval `(a, a+p)`.
|
toIcoMod_eq_iff
theorem toIcoMod_eq_iff :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) {a b c : α},
toIcoMod hp a b = c ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p
This theorem states that for any type `α` which forms a linear ordered additive commutative group and is Archimedean, given a positive `p`, and any three elements `a`, `b`, `c` of type `α`, the function `toIcoMod` applied to `p`, `a` and `b` being equal to `c` is equivalent to `c` belonging to the left-closed right-open interval from `a` to `a + p` and there existing an element `z` such that `b = c + z • p`. In simpler terms, it says that a number `b` reduced to the interval `a` to `a + p` equals `c` if and only if `c` lies in the interval `a` to `a + p` and `b` can be expressed as `c` plus some multiple of `p`.
More concisely: For any Archimedean, additively commutative and linearly ordered type `α` and positive element `p` in `α`, the element `c` belongs to the left-closed right-open interval `[a, a + p)` if and only if there exists an element `z` such that `b = c + z * p`.
|
sub_toIcoDiv_zsmul_mem_Ico
theorem sub_toIcoDiv_zsmul_mem_Ico :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α),
b - toIcoDiv hp a b • p ∈ Set.Ico a (a + p)
This theorem states that for any given type `α` which is a linear ordered additive commutative group and satisfies the Archimedean property, and for any positive `p` of type `α`, and any `a` and `b` of type `α`, the result of subtracting `p` times the unique integer (which is given by the function `toIcoDiv`) from `b` lies in the semi-open interval from `a` to `a + p`. In other words, after we subtract `p` multiplied by this unique integer from `b`, the resulting value will always be greater than or equal to `a` and less than `a + p`.
More concisely: For any Archimedean linear ordered additive commutative group `α`, positive `p` in `α`, and `a, b` in `α`, the result of subtracting `p` times the unique integer `n` with `b = a + p * n` is in the semi-open interval `(a, a + p)`.
|