mk_one

Mathlib.Data.PNat.Defs

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

English

In positive naturals, the element formed by 1 together with any witness is equal to 1.

Русский

В положительных натуральных числах элемент ⟨1, h⟩ равен 1 для любого доказательства h.

LaTeX

$$$\\forall h \, (\\langle 1, h \\rangle \\colon \\mathbb{N}^+) = (1 \\colon \\mathbb{N}^+)$$$

Lean4

@[simp]
theorem mk_one {h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+) :=
  rfl

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

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

Разделы

Аффилиация

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