disjoint_filter_filter_neg — Mathlib

English

Disjoint (S.filter p) (T.filter (not p)) for predicate p.

Русский

Непересечение (S.filter p) и (T.filter (не p)).

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{filter}(p, S), \\operatorname{filter}(\\lambda x, \\neg p(x), T))$$$

Lean4

theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
    Disjoint (s.filter p) (t.filter fun a => ¬p a) :=
  disjoint_filter_filter' s t disjoint_compl_right

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