English
If α is nonempty, and f : ι → Filter α is directed with every f(i) nontrivial, then iInf f is nontrivial.
Русский
Если α непустой и f : ι → Filter α направлено, каждая f(i) непустая, то iInf f непуст.
LaTeX
$$⟨Nonempty α⟩ → (Directed (· ≥ ·) f) → (∀ i, NeBot (f i)) → NeBot (iInf f)$$
Lean4
/-- If `f : ι → Filter α` is directed, `α` is not empty, and `∀ i, f i ≠ ⊥`, then `iInf f ≠ ⊥`.
See also `iInf_neBot_of_directed'` for a version assuming `Nonempty ι` instead of `Nonempty α`. -/
theorem iInf_neBot_of_directed {f : ι → Filter α} [hn : Nonempty α] (hd : Directed (· ≥ ·) f) (hb : ∀ i, NeBot (f i)) :
NeBot (iInf f) := by
cases isEmpty_or_nonempty ι
· constructor
simp [iInf_of_empty f, top_ne_bot]
· exact iInf_neBot_of_directed' hd hb
