pnatEquivNat — Mathlib

English

There exists a bijection between positive naturals and naturals given by n ↦ n−1 and its inverse m ↦ m+1.

Русский

Существует биекция между положительными натуральными числами и натуральными числами, задаваемая переходом n ↦ n−1 и обратной функцией m ↦ m+1.

LaTeX

$$$\\text{Equiv}(\\mathbb{N}^+ , \\mathbb{N}) \\text{ with } f(n)=n-1, g(m)=m+1$$$

Lean4

/-- An equivalence between `ℕ+` and `ℕ` given by `PNat.natPred` and `Nat.succPNat`. -/
@[simps -fullyApplied]
def _root_.Equiv.pnatEquivNat : ℕ+ ≃ ℕ where
  toFun := PNat.natPred
  invFun := Nat.succPNat
  left_inv := PNat.succPNat_natPred
  right_inv := Nat.natPred_succPNat

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