orderIsoNatOfLinearSuccPredArch — Mathlib

English

If there is a bottom and no top, there is an order isomorphism between ι and the natural numbers given by toZ.

Русский

Если существует нижняя граница и нет верхней границы, то существует каноническое изоморфизм порядка между ι и ℕ, задаваемый toZ.

LaTeX

$$ι ≃o ℕ$$

Lean4

/-- If the order has a bot but no top, `toZ` defines an `OrderIso` between `ι` and `ℕ`. -/
def orderIsoNatOfLinearSuccPredArch [NoMaxOrder ι] [OrderBot ι] : ι ≃o ℕ
    where
  toFun i := (toZ ⊥ i).toNat
  invFun n := succ^[n] ⊥
  left_inv
    i := by
    dsimp only
    exact iterate_succ_toZ i bot_le
  right_inv
    n := by
    dsimp only
    rw [toZ_iterate_succ]
    exact Int.toNat_natCast n
  map_rel_iff' := by
    intro i j
    simp only [Equiv.coe_fn_mk, Int.toNat_le]
    rw [← @toZ_le_iff ι _ _ _ _ ⊥, Int.toNat_of_nonneg (toZ_nonneg bot_le)]

Похожие утверждения