filter_cons_of_pos — Mathlib

English

If a ∉ s and p(a) holds, then filter p (cons a s ha) = {a} ∪ filter p s.

Русский

Если a ∉ s и p(a) истинно, то filter p (a :: s) = {a} ∪ filter p s.

LaTeX

$$$\\operatorname{filter}(p, \\{a\\} \\cup S) = \\{a\\} \\cup \\operatorname{filter}(p, S)$$$

Lean4

theorem filter_cons_of_pos (a : α) (s : Finset α) (ha : a ∉ s) (hp : p a) :
    filter p (cons a s ha) = cons a (filter p s) ((mem_of_mem_filter _).mt ha) :=
  eq_of_veq <| Multiset.filter_cons_of_pos s.val hp

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