English
If ι has both a bot and a top, there exists an order isomorphism between ι and Finset.range(N) for some finite N, via toZ.
Русский
Если в порядке ι есть нижняя и верхняя границы, то существует факторное отображение между ι и конечным диапазоном Finset.range(N) через toZ.
LaTeX
$$ι ≃o Finset.range (toZ ⊥ ⊤).toNat + 1$$
Lean4
/-- If the order has both a bot and a top, `toZ` gives an `OrderIso` between `ι` and
`Finset.range n` for some `n`. -/
def orderIsoRangeOfLinearSuccPredArch [OrderBot ι] [OrderTop ι] : ι ≃o Finset.range ((toZ ⊥ (⊤ : ι)).toNat + 1)
where
toFun i := ⟨(toZ ⊥ i).toNat, Finset.mem_range_succ_iff.mpr (Int.toNat_le_toNat ((toZ_le_iff _ _).mpr le_top))⟩
invFun n := succ^[n] ⊥
left_inv i := iterate_succ_toZ i bot_le
right_inv
n := by
ext1
simp only
refine le_antisymm ?_ ?_
· rw [Int.toNat_le]
exact toZ_iterate_succ_le _
by_cases hn_max : IsMax (succ^[↑n] (⊥ : ι))
· rw [← isTop_iff_isMax, isTop_iff_eq_top] at hn_max
rw [hn_max]
exact Nat.lt_succ_iff.mp (Finset.mem_range.mp n.prop)
· rw [toZ_iterate_succ_of_not_isMax _ hn_max]
simp only [Int.toNat_natCast, le_refl]
map_rel_iff' := by
intro i j
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]
rw [← @toZ_le_iff ι _ _ _ _ ⊥, Int.toNat_of_nonneg (toZ_nonneg bot_le)]
