mk

Mathlib.SetTheory.Ordinal.Notation

URI: https://scilib.ai/kg/mathlib#NONote.mk

Lean4

/-- Construct a `NONote` from an ordinal notation (and infer normality) -/
def mk (o : ONote) [h : ONote.NF o] : NONote :=
  ⟨o, h⟩

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

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

Разделы

Аффилиация

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