filter_eq_self — Mathlib

English

The filtered set equals the original if and only if every element of the original set satisfies the predicate.

Русский

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

LaTeX

$$$s.filter p = s \\Leftrightarrow \\forall x \\in s, p x$$$

Lean4

@[simp]
theorem filter_eq_self : s.filter p = s ↔ ∀ x ∈ s, p x := by simp [Finset.ext_iff]

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