pnatIsoNat — Mathlib

English

The order isomorphism between ℕ and ℕ+ given by succ.

Русский

Порядковый изоморфизм между ℕ и ℕ+, задаваемый succ.

LaTeX

$$$ (\\\\mathbb{N}^+, \\le) \\\\cong_o (\\\\mathbb{N}, \\le) \\\\text{ via } n \\mapsto n+1 \\text{ and inverse } k \\mapsto k-1. $$$

Lean4

/-- The order isomorphism between ℕ and ℕ+ given by `succ`. -/
@[simps! -fullyApplied apply]
def _root_.OrderIso.pnatIsoNat : ℕ+ ≃o ℕ where
  toEquiv := Equiv.pnatEquivNat
  map_rel_iff' := natPred_le_natPred

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