powerset

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.powerset

English

The powerset 𝒫 s consists of all subsets of s: 𝒫 s = { t ⊆ s }.

Русский

Множество 𝒫 s состоит из всех подмножеств s: 𝒫 s = { t ⊆ s }.

LaTeX

$$$\mathcal{P}(s) = \{t \mid t \subseteq s\}$$$

Lean4

/-- `𝒫 s` is the set of all subsets of `s`. -/
def powerset (s : Set α) : Set (Set α) :=
  {t | t ⊆ s}

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

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

Разделы

Аффилиация

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