cardinalInterFilter_principal

Mathlib.Order.Filter.CardinalInter

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

English

For any set s, the principal filter on s has the cardinal-intersection property at c.

Русский

Для любого множества s фильтр principal s имеет свойство пересечения по кардиналу c.

LaTeX

$$$\\mathrm{cardinalInterFilter\_principal}(s, c)$$$

Lean4

instance cardinalInterFilter_principal (s : Set α) : CardinalInterFilter (𝓟 s) c :=
  ⟨fun _ _ hS => subset_sInter hS⟩

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

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

Разделы

Аффилиация

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