enumOrd_zero

Mathlib.SetTheory.Ordinal.Enum

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

English

For any set s of ordinals, the 0-th element of its enumeration equals the infimum of s.

Русский

Для множества ординалов s нулевой элемент перечисления равен инфимууму s.

LaTeX

$$$\\mathrm{enumOrd} s 0 = \\mathrm{sInf} s$$$

Lean4

@[simp]
theorem enumOrd_zero : enumOrd s 0 = sInf s := by
  rw [enumOrd]
  simp [Ordinal.not_lt_zero]

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

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

Разделы

Аффилиация

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