enumIsoToType — Mathlib

English

For any ordinal o, there exists an order isomorphism between Set.Iio o and o.toType.

Русский

Для любого ординала o существует моноидный изоморфизм порядка между Set.Iio o и o.toType.

LaTeX

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

Lean4

/-- The order isomorphism between ordinals less than `o` and `o.toType`. -/
@[simps! -isSimp]
noncomputable def enumIsoToType (o : Ordinal) : Set.Iio o ≃o o.toType
    where
  toFun x := enum (α := o.toType) (· < ·) ⟨x.1, type_toType _ ▸ x.2⟩
  invFun x := ⟨typein (α := o.toType) (· < ·) x, typein_lt_self x⟩
  left_inv _ := Subtype.ext (typein_enum _ _)
  right_inv _ := enum_typein _ _
  map_rel_iff' := enum_le_enum' _

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