filter_nonempty_iff — Mathlib

English

A nonempty filter corresponds to the existence of an element in the original set that satisfies the predicate.

Русский

Не пустой фильтр соответствует существованию элемента в исходном множестве, удовлетворяющего предикату.

LaTeX

$$$(s.filter p).Nonempty \\iff \\exists a \\in s, p a$$$

Lean4

theorem filter_nonempty_iff : (s.filter p).Nonempty ↔ ∃ a ∈ s, p a := by
  simp only [nonempty_iff_ne_empty, Ne, filter_eq_empty_iff, Classical.not_not, not_forall, exists_prop]

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