Theorems · Theorem · combinatorics

Multiset.countP_congr

∀ {α : Type u_1} {s s' : Multiset α},
  s = s' →
    ∀ {p p' : α → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred p'],
      (∀ x ∈ s, p x = p' x) → Multiset.countP p s = Multiset.countP p' s'

Defined in

Mathlib.Data.Multiset.Count

Cited by

4 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

DecidablePredDecidablePred