Theorems · Theorem · order theory

Multiset.filter_inter

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

Defined in

Mathlib.Data.Multiset.UnionInter

Cited by

0 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidablePred