English
Let f = (f i) be a family of filters on each α i and s = (s i) a family of subsets of α i. Then the filter pi f, intersected with the principal filter generated by the product set Set.pi univ s, is non-bottom if and only if every component f i intersected with the principal filter generated by s i is non-bottom.
Русский
Пусть f = (f i) — семейство фильтров на соответствующих множествах α i, и s = (s i) — семейство подмножеств α i. Тогда фильтр π f, пересечённый с простейшим фильтром, порождённым множеством Set.pi univ s, не равен нижнему пределу тогда и лишь тогда каждый компонент f i ⊓ 𝓟(s i) ненизко(непустой).
LaTeX
$$$\\operatorname{NeBot}\\left(\\pi f \\;\\inf\\; \\mathcal{P}\\left(\\mathrm{Set.pi\\ univ\\ } s\\right)\\right) \\iff \\forall i, \\operatorname{NeBot}\\left(f i \\;\\inf\\; \\mathcal{P}\\left(s i\\right)\\right)$$$
Lean4
@[simp]
theorem pi_inf_principal_univ_pi_neBot : NeBot (pi f ⊓ 𝓟 (Set.pi univ s)) ↔ ∀ i, NeBot (f i ⊓ 𝓟 (s i)) := by
simp [neBot_iff]
