PartENat

Mathlib.Data.Nat.PartENat

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

Lean4

/-- Type of natural numbers with infinity (`⊤`) -/
@[deprecated ENat (since := "2025-09-01")]
def PartENat : Type :=
  Part ℕ

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

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

Разделы

Аффилиация

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