term_ord_aux

Mathlib.Topology.Category.Profinite.Nobeling.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.term_ord_aux

← MathLib Explorer

English

For any o and ho with o < type(...), ord I (term I ho) = o.

Русский

Для любого o и ho с ho: o < type(...) выполняется ord I(term I ho) = o.

LaTeX

$$$\\forall o,\\ ho: o < \\mathrm{type}((<)) \\;\\Rightarrow\\; \\mathrm{ord}_I(\\mathrm{term}_I(ho)) = o.$$$

Lean4

theorem term_ord_aux {i : I} (ho : ord I i < Ordinal.type ((· < ·) : I → I → Prop)) : term I ho = i := by
  simp only [term, ord, Ordinal.enum_typein]

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

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

Разделы

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

Аффилиация

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