le_enum_succ — Mathlib

English

In the successor o, every a in (succ o).toType is less than or equal to the element given by the enumeration at index o.

Русский

В следующем ординале o каждый элемент a из (succ o).toType не превосходит элемент, получаемый перечислением по индексу o.

LaTeX

$$$\forall a \in (\text{succ } o).\toType,\ a \le \mathrm{enum}(\cdot<\cdot)\langle o, \cdot \rangle$$$

Lean4

theorem le_enum_succ {o : Ordinal} (a : (succ o).toType) :
    a ≤ enum (α := (succ o).toType) (· < ·) ⟨o, (type_toType _ ▸ lt_succ o)⟩ :=
  by
  rw [← enum_typein (α := (succ o).toType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk, ← lt_succ_iff]
  apply typein_lt_self

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