small_set

Mathlib.Logic.Small.Basic

URI: https://scilib.ai/kg/mathlib#small_set

English

If α is small, then Set α is small.

Русский

Если α мала, то множество α мало.

LaTeX

$$$ \\text{Small}(\\operatorname{Set}\\,\\alpha) $$$

Lean4

instance small_set {α} [Small.{w} α] : Small.{w} (Set α) :=
  ⟨⟨Set (Shrink α), ⟨Equiv.Set.congr (equivShrink α)⟩⟩⟩

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

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

Разделы

Аффилиация

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