typein_one_toType

Mathlib.SetTheory.Ordinal.Basic

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

English

For every x in toType 1, typein(x) equals 0.

Русский

Для любого x∈toType(1) typein(x) = 0.

LaTeX

$$$\forall x : toType(1),\ \operatorname{typein}(x) = 0$$$

Lean4

@[simp]
theorem typein_one_toType (x : toType 1) : typein (α := toType 1) (· < ·) x = 0 := by rw [one_toType_eq x, typein_enum]

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

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

Разделы

Аффилиация

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