succPNat_inj

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#Nat.succPNat_inj

English

Let n,m ∈ ℕ. Then succPNat(n) = succPNat(m) if and only if n = m.

Русский

Пусть n,m ∈ ℕ. Тогда succPNat(n) = succPNat(m) тогда и только тогда, когда n = m.

LaTeX

$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\; \\\\text{succPNat}(n)=\\\\text{succPNat}(m) \\\\\\iff n=m.$$$

Lean4

@[simp]
theorem succPNat_inj {n m : ℕ} : succPNat n = succPNat m ↔ n = m :=
  succPNat_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru