ofENat

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.ofENat

← MathLib Explorer

English

For any n in ℕ∞, toWithTop(↑n) = n.

Русский

Для любого n ∈ ℕ∞, toWithTop(↑n) = n.

LaTeX

$$$\\\\operatorname{toWithTop}(\\\\uparrow n) = n \\\\text{ for } n \\in \\mathbb{N}_{\\infty}$$$

Lean4

/-- Coercion from `ℕ∞` to `PartENat`. -/
@[coe]
def ofENat : ℕ∞ → PartENat := fun x =>
  match x with
  | Option.none => none
  | Option.some n => some n

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

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

Разделы

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

Аффилиация

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