card_eq_countP_add_countP — Mathlib

English

The cardinality of s equals the sum of the p-count and the not-p-count: card s = countP p s + countP (not p) s.

Русский

Кардинальность s равна сумме подсчетов по p и по не-p: card s = countP p s + countP (not p) s.

LaTeX

$$$\operatorname{card}(s) = \operatorname{countP}(p, s) + \operatorname{countP}(\lambda x. \neg p(x), s)$$$

Lean4

theorem card_eq_countP_add_countP (s) : card s = countP p s + countP (fun x => ¬p x) s :=
  Quot.inductionOn s fun l => by simp [l.length_eq_countP_add_countP p]

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