English
Let f : i ↦ Filter(α i) be a family of filters, s : i ↦ Set(α i), and I a subset of ι. If every f i is non-bottom, then NeBot of the product pi f intersected with the principal filter on (I.pi s) is equivalent to NeBot for all i in I of (f i ⊓ 𝓟(s i)).
Русский
Пусть f : i ↦ фильтр(α i), s : i ↦ множество(α i), I ⊆ ι. Если каждый f i не нижний, тогда не нижний произведения pi f ∩ 𝓟(I.pi s) эквивалентен для всех i ∈ I того, что f i ⊓ 𝓟(s i) не нижний.
LaTeX
$$$\\forall i, NeBot\\left(f i\\right) \\Rightarrow\\ leftarrow NeBot\\left(\\pi f \\inf \\mathcal{P}\\left(I.\\pi s\\right)\\right) \\iff \\forall i \\in I, NeBot\\left(f i \\inf \\mathcal{P}\\left(s i\\right)\\right)$$$
Lean4
@[simp]
theorem pi_inf_principal_pi_neBot [∀ i, NeBot (f i)] {I : Set ι} :
NeBot (pi f ⊓ 𝓟 (I.pi s)) ↔ ∀ i ∈ I, NeBot (f i ⊓ 𝓟 (s i)) := by simp [neBot_iff]
