small_Iio — Mathlib

English

There is a canonical order isomorphism between the initial segment of ordinals and the type o.toType.

Русский

Существует канонический порядок-изоморфизм между начальным отрезком ординалов и типом o.toType.

LaTeX

$$$\\mathrm{enumIsoToType}(o) : \\mathrm{Set.Iio}(o) \\simeq_o o.toType$$$

Lean4

instance small_Iio (o : Ordinal.{u}) : Small.{u} (Iio o) :=
  ⟨_, ⟨(enumIsoToType _).toEquiv⟩⟩

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