smallSets_principal

Mathlib.Order.Filter.SmallSets

URI: https://scilib.ai/kg/mathlib#Filter.smallSets_principal

English

The smallSets of a principal filter on s equals the principal of the power set of s.

Русский

Малые множества приземленного фильтра на s равны приземленному фильтру над мощсетами s.

LaTeX

$$$ (\\\\mathcal P s).smallSets = \\\\mathcal P (\\\\mathcal P s) $$$

Lean4

@[simp]
theorem smallSets_principal (s : Set α) : (𝓟 s).smallSets = 𝓟 (𝒫 s) :=
  lift'_principal monotone_powerset

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

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

Разделы

Аффилиация

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