rank_eq_typein — Mathlib

English

For a well-order r, rank r equals the type of r, i.e., rank r = typein r.

Русский

Для хорошо упорядоченного отношения r равенство: rank r = typein r.

LaTeX

$$$\operatorname{rank} r = \operatorname{typein} r$$$

Lean4

@[simp]
theorem rank_eq_typein (r) [IsWellOrder α r] : rank r = Ordinal.typein r := by
  classical
  letI := linearOrderOfSTO r
  ext a
  exact
    InitialSeg.eq
      (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding, fun a b h ↦
        mem_range_rank_of_le h.le⟩)
      (Ordinal.typein r) a

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