small_Iic

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

For every a ∈ NatOrdinal, Set.Iic a is small.

Русский

Для каждого a ∈ NatOrdinal, Set.Iic(a) мало по мощности.

LaTeX

$$$\\forall a:\\mathrm{NatOrdinal},\\ \\operatorname{Small}(\\mathrm{Set.Iic}(a))$$$

Lean4

instance small_Iic (a : NatOrdinal.{u}) : Small.{u} (Set.Iic a) :=
  Ordinal.small_Iic a

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

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

Разделы

Аффилиация

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