iInf_neBot_iff_of_directed — Mathlib

English

If α is nonempty, for directed f, iInf f is nontrivial iff ∀ i, f i is nontrivial.

Русский

Если α непустой и f направлено, то iInf f непуст тогда и только тогда, когда все f(i) непусты.

LaTeX

$$iInf_neBot_iff_of_directed {f : ι → Filter α} [Nonempty α] (hd : Directed (· ≥ ·) f) : NeBot (iInf f) ↔ ∀ i, NeBot (f i)$$

Lean4

theorem iInf_neBot_iff_of_directed {f : ι → Filter α} [Nonempty α] (hd : Directed (· ≥ ·) f) :
    NeBot (iInf f) ↔ ∀ i, NeBot (f i) :=
  ⟨fun H i => H.mono (iInf_le _ i), iInf_neBot_of_directed hd⟩

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