small_Iic

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.small_Iic

English

For any ordinal o, the set Iio(o) is a small type.

Русский

Для любого ординала o множество Iio(o) является маленьким типом.

LaTeX

$$Small( Set.Iio(o).Elem )$$

Lean4

instance small_Iic (o : Ordinal.{u}) : Small.{u} (Iic o) :=
  by
  rw [← Iio_union_right]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru