iInf_neBot_of_directed' — Mathlib

English

If f : ι → Filter α is directed and nonempty, and every f(i) is nontrivial, then iInf f is nontrivial.

Русский

Если f : ι → Filter α направлено и непусто, и каждый f(i) непуст, то iInf f непуст.

LaTeX

$$(∀ i, (f i)).NeBot → (iInf f).NeBot$$

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 α} [Nonempty ι] (hd : Directed (· ≥ ·) f) :
    (∀ i, NeBot (f i)) → NeBot (iInf f) :=
  not_imp_not.1 <| by simpa only [not_forall, not_neBot, ← empty_mem_iff_bot, mem_iInf_of_directed hd] using id

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