filter_eq_empty_iff — Mathlib

English

The filtered set is empty if and only if no element of the original set satisfies the predicate.

Русский

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

LaTeX

$$$s.filter p = \\emptyset \\iff \\forall x \\in s, \\neg p x$$$

Lean4

@[simp]
theorem filter_eq_empty_iff : s.filter p = ∅ ↔ ∀ ⦃x⦄, x ∈ s → ¬p x := by simp [Finset.ext_iff]

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