typein_lt_self

Mathlib.SetTheory.Ordinal.Basic

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

English

For any a in α, typein r a < type r holds.

Русский

Для любого элемента a в α: typein r a < type r.

LaTeX

$$$\forall a:\; a\in α:\; typein r a < type r$$$

Lean4

theorem typein_lt_self {o : Ordinal} (i : o.toType) : typein (α := o.toType) (· < ·) i < o :=
  by
  simp_rw [← type_toType o]
  apply typein_lt_type

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

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

Разделы

Аффилиация

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