filter_not — Mathlib

English

Let s be a finite set and p a predicate. Then filtering by not p yields the complement relative to s: filter (fun a => ¬p a) s = s \\ filter p s.

Русский

Пусть s — конечное множество, а предикат p. Тогда фильтрация по не-p даёт разность s и фильтрованного p: filter (¬p) s = s \\ filter p s.

LaTeX

$$$\\operatorname{filter} (\\lambda a. \\neg p a)\\, s = s \\setminus \\operatorname{filter} p\\, s$$

Lean4

theorem filter_not (s : Finset α) : (s.filter fun a => ¬p a) = s \ s.filter p := by grind

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