toType_empty_iff_eq_zero

Mathlib.SetTheory.Ordinal.Basic

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

← MathLib Explorer

English

The type equality for toType and empty implies empty equivalence.

Русский

Эквивалентность типов для toType и пустого типа приводит к равенству нулю.

LaTeX

$$$\mathrm{toTypeEmpty}(o) \,\Rightarrow \, o = 0$$$

Lean4

@[simp]
theorem toType_empty_iff_eq_zero {o : Ordinal} : IsEmpty o.toType ↔ o = 0 := by
  rw [← @type_eq_zero_iff_isEmpty o.toType (· < ·), type_toType]

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

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

Разделы

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

Аффилиация

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