coe_injective

Mathlib.Data.PNat.Defs

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

← MathLib Explorer

English

The map PNat.val : PNat → ℕ is injective.

Русский

Отображение PNat.val : PNat → ℕ инъективно.

LaTeX

$$$ \\operatorname{val}: \\mathbb{N}^+ \\to \\mathbb{N} \\text{ is injective},$ i.e., $\\forall m,n \\in \\mathbb{N}^+,\\; m.v = n.v \\Rightarrow m = n.$$$

Lean4

theorem coe_injective : Function.Injective PNat.val :=
  Subtype.coe_injective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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