smallSets_iInf

Mathlib.Order.Filter.SmallSets

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

English

(iInf f).smallSets equals the infimum over i of (f(i)).smallSets.

Русский

Малые множества iInf f равны инфимума по i от (f(i)).smallSets.

LaTeX

$$$ (\\\\iInf f).smallSets = \\\\inf i, (f i).smallSets $$$

Lean4

theorem smallSets_iInf {f : ι → Filter α} : (iInf f).smallSets = ⨅ i, (f i).smallSets :=
  lift'_iInf_of_map_univ (powerset_inter _ _) powerset_univ

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

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

Разделы

Аффилиация

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