orderIsoOfNat — Mathlib

English

There exists an order isomorphism between ℕ and any infinite subset s of ℕ.

Русский

Существует изоморфизм порядка между ℕ и любым бесконечным подмножеством ℕ.

LaTeX

$$$$\mathrm{orderIsoOfNat}(s) : \mathbb{N} \cong_o s.$$$$

Lean4

/-- `Nat.Subtype.ofNat` as an order isomorphism between `ℕ` and an infinite subset. See also
`Nat.Nth` for a version where the subset may be finite. -/
noncomputable def orderIsoOfNat : ℕ ≃o s := by
  classical
    exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective

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