sub_filter_eq_filter_not — Mathlib

English

Removing the elements of s that satisfy a predicate p from s is the same as keeping the elements that do not satisfy p.

Русский

Исключение элементов s, удовлетворяющих p, эквивалентно сохранению элементов, не удовлетворяющих p.

LaTeX

$$$ s - s.filter p = s.filter (\\lambda a, \\neg p a) $$$

Lean4

@[simp]
theorem sub_filter_eq_filter_not (p : α → Prop) [DecidablePred p] (s : Multiset α) :
    s - s.filter p = s.filter fun a ↦ ¬p a := by ext a; by_cases h : p a <;> simp [h]

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