enum_succ_eq_top — Mathlib

English

For any ordinal o, the enumeration of the order on (succ o).toType yields the top element.

Русский

Для любого ординала o перечисление порядка на (succ o).toType даёт верхний элемент.

LaTeX

$$$$ \operatorname{enum}_{\alpha := (\mathrm{succ} o).\mathrm{toType}}(\cdot < \cdot)\;\langle o, \mathrm{type\_toType}\_ , \lt\_succ o\rangle = \top $$$$

Lean4

theorem enum_succ_eq_top {o : Ordinal} : enum (α := (succ o).toType) (· < ·) ⟨o, type_toType _ ▸ lt_succ o⟩ = ⊤ :=
  rfl

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