iInf_neBot_iff_of_directed' — Mathlib

English

For f : ι → Filter α and directed f, (iInf f).NeBot iff ∀ i, (f i).NeBot.

Русский

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

LaTeX

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

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⟩

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