smallSets_inf

Mathlib.Order.Filter.SmallSets

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

English

The smallSets of the infimum of two filters equals the infimum of their smallSets.

Русский

Малые множества инфима двух фильтров равны инфимума их малых множеств.

LaTeX

$$$ (l_1 \\\\inf l_2).smallSets = l_1.smallSets \\\\inf l_2.smallSets $$$

Lean4

theorem smallSets_inf (l₁ l₂ : Filter α) : (l₁ ⊓ l₂).smallSets = l₁.smallSets ⊓ l₂.smallSets :=
  lift'_inf _ _ powerset_inter

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

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

Разделы

Аффилиация

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