filter_union_filter_neg_eq — Mathlib

English

If for all x the negation is decidable, then the union of filters by p and not p equals the original set: (s.filter p ∪ s.filter (not p)) = s.

Русский

Если для каждого элемента x решаемо, то объединение фильтров по p и не p даёт исходное множество: (s.filter p ∪ s.filter (¬p)) = s.

LaTeX

$$$\\operatorname{filter} p\\, s \\cup \\operatorname{filter} (\\lnot p)\\, s = s$$$

Lean4

theorem filter_union_filter_neg_eq [∀ x, Decidable (¬p x)] (s : Finset α) : (s.filter p ∪ s.filter fun a => ¬p a) = s :=
  filter_union_filter_of_codisjoint _ _ _ <| @codisjoint_hnot_right _ _ p

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