countableInterFilter_principal

Mathlib.Order.Filter.CountableInter

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

English

The principal filter on a set s is a CountableInterFilter.

Русский

Принципиальный фильтр над множеством s является CountableInterFilter.

LaTeX

$$$\\text{countableInterFilter_principal}(s) : CountableInterFilter (\\mathcal{P}(s))$$$

Lean4

instance countableInterFilter_principal (s : Set α) : CountableInterFilter (𝓟 s) :=
  ⟨fun _ _ hS => subset_sInter hS⟩

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

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

Разделы

Аффилиация

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