iSup_neBot — Mathlib

English

The supremum of a family of filters is nontrivial iff some member is nontrivial.

Русский

Супремум семейства фильтров не тривиален тогда и только тогда, когда некоторый член не тривиален.

LaTeX

$$$(\bigvee_i f_i).\mathrm{NeBot} \iff \exists i, (f_i).\mathrm{NeBot}$$$

Lean4

@[simp]
theorem iSup_neBot {f : ι → Filter α} : (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot := by simp [neBot_iff]

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