toZ_nonneg
theorem toZ_nonneg :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 i : ι}, i0 ≤ i → 0 ≤ toZ i0 i
The theorem `toZ_nonneg` states that for any type `ι` equipped with a linear order, a successor order, a predecessor order, and the Archimedean property for successors, if `i0` and `i` are elements of `ι` such that `i0` is less than or equal to `i`, then the integer value obtained by applying the `toZ` function to `i0` and `i` is nonnegative. In other words, the function `toZ` produces a nonnegative integer when its second argument is greater than or equal to its first argument.
More concisely: For any type equipped with a linear order, successor order, predecessor order, and the Archimedean property for successors, the integer value obtained from any element less than or equal to another element using the `toZ` function is nonnegative.
|
iterate_pred_toZ
theorem iterate_pred_toZ :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 : ι}, ∀ i < i0, Order.pred^[(-toZ i0 i).toNat] i0 = i
This theorem, `iterate_pred_toZ`, states that for any type `ι` with a linear order, a successor order, a predecessor order, and satisfying the Archimedean property, given a base element `i0` of `ι`, and any other element `i` that is less than `i0`, applying the predecessor function `Order.pred` to `i0` as many times as the absolute value of the integer returned from the order function `toZ` applied to `i0` and `i`, will yield `i`. In other words, we can reach `i` from `i0` by repeatedly applying the predecessor function the number of times determined by the order between `i0` and `i`.
More concisely: For any type `ι` with a linear order, successor, predecessor, and the Archimedean property, for all `i0 i` with `i < i0`, we have `i = Order.iterate_pred i0 (toZ (i0 - i))`.
|
toZ_of_lt
theorem toZ_of_lt :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 i : ι} (hi : i < i0), toZ i0 i = -↑(Nat.find ⋯)
The theorem `toZ_of_lt` states that for any type `ι` that has a linear order, a successor order, satisfies the Archimedean property, and has a predecessor order, and for any two elements `i0` and `i` of this type such that `i` is less than `i0`, the function `toZ` applied to `i0` and `i` equals the negative of a certain natural number (found using `Nat.find`). In other words, if `i` is less than `i0`, `toZ` assigns it a negative integer value.
More concisely: For any type with a linear order, successor, Archimedean property, and a predecessor order, the function `toZ` maps elements less than another element to the negative of a corresponding natural number.
|
toZ_of_ge
theorem toZ_of_ge :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 i : ι} (hi : i0 ≤ i), toZ i0 i = ↑(Nat.find ⋯)
The theorem `toZ_of_ge` states that for all types ι with a linear order, a successor order, an Archimedean successor property, and a predecessor order, and for all elements i0 and i of type ι such that i0 is less than or equal to i, the function `toZ` applied to i0 and i returns the integer representation of the value obtained by applying the `Nat.find` function to some unspecified argument.
More concisely: For all types ι with a linear order, successor order, Archimedean successor property, and a predecessor order, the function `toZ` maps the predecessor of any element i to the integer representation of the index of i in the order.
|
toZ_le_iff
theorem toZ_le_iff :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 : ι} (i j : ι), toZ i0 i ≤ toZ i0 j ↔ i ≤ j
The theorem `toZ_le_iff` states that for any type `ι` under certain conditions - it has a linear order, it has a successor order, it is Archimedean with respect to the successor function, and it has a predecessor order - and for any `i0`, `i`, and `j` of this type, the integer value of `toZ i0 i` is less than or equal to the integer value of `toZ i0 j` if and only if `i` is less than or equal to `j`. In other words, the function `toZ` preserves the order of elements in `ι`.
More concisely: For any type `ι` satisfying certain conditions, the function `toZ : ι → ℤ` preserves order, i.e., `toZ i0 ≤ toZ i1` if and only if `i0 ≤ i1` for all `i0, i1 : ι`.
|
LinearLocallyFiniteOrder.succFn_spec
theorem LinearLocallyFiniteOrder.succFn_spec :
∀ {ι : Type u_1} [inst : LinearOrder ι] (i : ι), IsGLB (Set.Ioi i) (LinearLocallyFiniteOrder.succFn i)
The theorem `LinearLocallyFiniteOrder.succFn_spec` states that for any type ι that has a linear order, and for any element `i` of that type, the successor function `LinearLocallyFiniteOrder.succFn` provides a value that is a greatest lower bound (GLB) for the set of all elements greater than `i`. In other words, the result of the successor function is the smallest value that is greater than `i` in the given order, assuming such a value exists.
More concisely: For any linear order type ι and its element i, the successor function `LinearLocallyFiniteOrder.succFn` gives the greatest lower bound of elements greater than i.
|
iterate_succ_toZ
theorem iterate_succ_toZ :
∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
{i0 : ι} (i : ι), i0 ≤ i → Order.succ^[(toZ i0 i).toNat] i0 = i
This theorem states that for all types `ι` with a linear order, a successor order, a successor archimedean order, and a predecessor order, with a given initial element `i0`, and for any other element `i` in `ι` such that `i0` is less than or equal to `i`, applying the successor function to `i0` the number of times specified by converting `toZ` of `i0` and `i` to a natural number, you will obtain `i`. In other words, it says that you can get from `i0` to `i` by successively applying the successor function as many times as the natural number equivalent of `toZ` of `i0` and `i`.
More concisely: For all types `ι` with a linear order and an initial element `i0`, if `i` is any element with `i0 ≤ i`, then `i0` is the `toZ i0`-th successor of `i0`, i.e., `i = i0 ^ (toZ i0) ^... ^ (toZ i0) ^ i0` where the exponent `n` is equal to `toZ i i0` (the natural number representation of `i` and `i0`).
|