canLiftPNat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance canLiftPNat : CanLift ℤ ℕ+ (↑) ((0 < ·)) :=
  ⟨fun n hn =>
    ⟨Nat.toPNat' (Int.natAbs n), by rw [Nat.toPNat'_coe, if_pos (Int.natAbs_pos.2 hn.ne'), Int.natAbs_of_nonneg hn.le]⟩⟩

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