count_filter_of_pos — Mathlib

English

If p(a) holds, then counting a in the filter equals counting a in the original multiset.

Русский

Если p(a) истинно, то счёт a в фильтре равен счёту a во всём мультиете.

LaTeX

$$$p(a) \Rightarrow \operatorname{count} a (\operatorname{filter} p s) = \operatorname{count} a s$$$

Lean4

@[simp]
theorem count_filter_of_pos {p} [DecidablePred p] {a} {s : Multiset α} (h : p a) : count a (filter p s) = count a s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', filter_coe, coe_count]
    apply count_filter
    simpa using h

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