eq

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#PNat.eq

English

If the underlying naturals of two positive naturals are equal, then the positive naturals are equal.

Русский

Если основы naturals двух положительных чисел равны, то сами числа равны.

LaTeX

$$$ \\forall {m n : \\mathbb{N}^+},\\; (m : \\mathbb{N}) = n \\Rightarrow m = n.$$$

Lean4

theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n :=
  Subtype.eq

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

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

Разделы

Аффилиация

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