instOfNatPNatOfNeZeroNat — Mathlib

English

Every nonzero natural number can be regarded as an element of ℕ⁺ by the embedding n ↦ ⟨n, n > 0⟩.

Русский

Каждое ненулевое натуральное число можно рассматривать как элемент ℕ⁺ через вложение n ↦ ⟨n, n > 0⟩.

LaTeX

$$$ \\mathbb{N}_{>0} \\cong \\{ n \\in \\mathbb{N} \\mid n > 0 \\}. $$$$

Lean4

instance (n : ℕ) [NeZero n] : OfNat ℕ+ n :=
  ⟨⟨n, Nat.pos_of_ne_zero <| NeZero.ne n⟩⟩

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