enumOrd_range

Mathlib.SetTheory.Ordinal.Enum

URI: https://scilib.ai/kg/mathlib#Ordinal.enumOrd_range

← MathLib Explorer

English

If e does not appear among CNF b o exponents, then coeff b o e = 0.

Русский

Если e не встречается среди показателей CNF(b,o), то coeff(b,o,e) = 0.

LaTeX

$$$$ e \\notin (CNF(b,o)).map Prod.fst \\to\\; \\operatorname{coeff}(b,o,e) = 0 $$$$

Lean4

theorem enumOrd_range {f : Ordinal → Ordinal} (hf : StrictMono f) : enumOrd (range f) = f :=
  (eq_enumOrd _ hf.not_bddAbove_range_of_wellFoundedLT).2 ⟨hf, rfl⟩

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

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

Разделы

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

Аффилиация

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