filter_card_add_filter_neg_card_eq_card

English

Let s be a finite set and p a predicate with decidable truth values. Then the cardinalities of s filtered by p and by not p sum to the cardinality of s: |s filtered by p| + |s filtered by not p| = |s|.

Русский

Пусть s — конечное множество, а p — предикат с разрешимой для выбора истиной. Тогда кардинальности выборки s по p и по не p суммируются до кардинальности s.

LaTeX

$$$|s \\text{ filtered by } p| + |s \\text{ filtered by } \\neg p| = |s|$$$

Lean4

theorem filter_card_add_filter_neg_card_eq_card (p : α → Prop) [DecidablePred p] [∀ x, Decidable (¬p x)] :
    #(s.filter p) + #(s.filter fun a ↦ ¬p a) = #s := by
  classical rw [← card_union_of_disjoint (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]

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