toNat

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.toNat

English

Conversion from ℕ∞ to ℕ sending ∞ to 0.

Русский

Переобразование ℕ∞ в ℕ, отправляющее бесконечность в 0.

LaTeX

$$$\\\\operatorname{toNat}: \\mathbb{N}_{\\\\infty} \\\\to \\\\mathbb{N},\\\\ toNat(\\top)=0,\\\\ toNat(n)=n \\\\text{for finite } n.$$$

Lean4

/-- Conversion of `ℕ∞` to `ℕ` sending `∞` to `0`. -/
def toNat : ℕ∞ → ℕ :=
  WithTop.untopD 0

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

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

Разделы

Аффилиация

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