enum_zero_eq_bot — Mathlib

English

Let o be an ordinal with 0 < o. Then the canonical enumeration of the elements of o with the natural ordering has its first element equal to the bottom element of o.

Русский

Пусть o — ординал с 0 < o. Тогда каноническая пронумровка элементов o по естественному порядку имеет первый элемент, равный нижнему элементу o.

LaTeX

$$$\\text{If } 0 < o, \\text{ then } \\operatorname{enum}(\\alpha := o^{\\mathrm{toType}})(<)(0) = \\bot_{o^{\\mathrm{toType}}}.$$$

Lean4

theorem enum_zero_eq_bot {o : Ordinal} (ho : 0 < o) :
    enum (α := o.toType) (· < ·) ⟨0, by rwa [type_toType]⟩ =
      have H := toTypeOrderBot (o := o) (by rintro rfl; simp at ho)
      (⊥ : o.toType) :=
  rfl

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