English
The function toZ enumerates elements of a linear order by their order relative to a starting point, yielding an integer-valued index with forward and backward branches.
Русский
Функция toZ нумерует элементы линейного порядка относительно начальной точки, выдавая целочисленный индекс с двумя направленностями.
LaTeX
$$$\\mathrm{toZ}: (i_0,i) \\mapsto \\begin{cases} \\mathbb{Z} & \\text{if } i_0 \\le i \\\\ -\\mathbb{Z} & \\text{otherwise} \\end{cases}$$$
Lean4
/-- `toZ` numbers elements of `ι` according to their order, starting from `i0`. We prove in
`orderIsoRangeToZOfLinearSuccPredArch` that this defines an `OrderIso` between `ι` and
the range of `toZ`. -/
def toZ (i0 i : ι) : ℤ :=
dite (i0 ≤ i) (fun hi ↦ Nat.find (exists_succ_iterate_of_le hi)) fun hi ↦
-Nat.find (exists_pred_iterate_of_le (α := ι) (not_le.mp hi).le)
