countP_eq_countP_filter_add — Mathlib

English

CountP p s equals the sum of CountP p on the q-filtered part and on the not-q part.

Русский

CountP p s равно сумме CountP p на части, отфильтрованных по q и по не-q.

LaTeX

$$$\operatorname{countP} p s = \operatorname{countP} p (\operatorname{filter} q s) + \operatorname{countP} p (\operatorname{filter}(\lambda a. \lnot q a) s)$$$

Lean4

theorem countP_eq_countP_filter_add (s) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    countP p s = (filter q s).countP p + (filter (fun a => ¬q a) s).countP p :=
  Quot.inductionOn s fun l => by
    convert l.countP_eq_countP_filter_add (p ·) (q ·)
    simp

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