countP_attach — Mathlib

English

Attaching the elements of s preserves the countP: countP (fun a => p a) s.attach = countP p s.

Русский

Прикрепление элементов s сохраняет значение countP: countP (λ a, p a) s.attach = countP p s.

LaTeX

$$$\operatorname{countP}(\lambda a. p(a), s.\text{attach}) = \operatorname{countP}(p, s)$$$

Lean4

theorem countP_attach (s : Multiset α) : s.attach.countP (fun a : { a // a ∈ s } ↦ p a) = s.countP p :=
  Quotient.inductionOn s fun l =>
    by
    simp only [quot_mk_to_coe, coe_countP, coe_attach, coe_countP, ← List.countP_attach (l := l)]
    rfl

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