canLiftPNat — Mathlib

English

Every positive natural number arises from a positive natural via the canonical embedding.

Русский

Каждое положительное натуральное число возникает из положительного натурального через каноническое вложение.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\exists p \\in \\mathbb{N}^+ \\ ,\\uparrow p = n$$$

Lean4

instance canLiftPNat : CanLift ℕ ℕ+ (↑) (fun n => 0 < n) :=
  ⟨fun n hn => ⟨Nat.toPNat' n, PNat.toPNat'_coe hn⟩⟩

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