mk_coe

Mathlib.Data.PNat.Defs

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

English

The natural-number component of a positive natural ⟨n, h⟩ is n.

Русский

Достоинство натурального компонента положительного натурального числа ⟨n, h⟩ равно n.

LaTeX

$$$ \\forall n \\in \\mathbb{N}, \\forall h \\text{ with } h>0,\\; (\\langle n, h \\rangle : \\mathbb{N}) = n.$$$

Lean4

@[simp]
theorem mk_coe (n h) : (PNat.val (⟨n, h⟩ : ℕ+) : ℕ) = n :=
  rfl

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

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

Разделы

Аффилиация

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