small_powerset

Mathlib.Logic.Small.Set

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

English

If s is Small, then its powerset 𝒫 s is Small.

Русский

Если s мала, то 𝒫 s мала.

LaTeX

$$$Small(s) \Rightarrow Small(\mathcal{P}(s)).$$$

Lean4

instance small_powerset (s : Set α) [Small.{u} s] : Small.{u} (𝒫 s) :=
  small_map (Equiv.Set.powerset s)

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

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

Разделы

Аффилиация

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