Theorems · Theorem · combinatorics

Multiset.filter.congr_simp

∀ {α : Type u_1} (p p_1 : α → Prop),
  p = p_1 →
    ∀ {inst : DecidablePred p} [inst_1 : DecidablePred p_1] (s s_1 : Multiset α),
      s = s_1 → Multiset.filter p s = Multiset.filter p_1 s_1

Defined in

Mathlib.Data.Multiset.Filter

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidablePred