Filtering multisets by a predicate

Main definitions

• Multiset.filter: filter p s is the multiset of elements in s that satisfy p.
• Multiset.filterMap: filterMap f s is the multiset of bs where some b ∈ map f s.

Multiset.filter

def Multiset.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : Multiset α

Filter p s returns the elements in s (with the same multiplicities) which satisfy p, and removes the rest.

@[simp]

theorem Multiset.filter_coe {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : List α) : filter p ↑l = ↑(List.filter (fun (b : α) => decide (p b)) l)

@[simp]

theorem Multiset.filter_zero {α : Type u_1} (p : α → Prop) [DecidablePred p] : filter p 0 = 0

theorem Multiset.filter_congr {α : Type u_1} {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} : (∀ (x : α), x ∈ s → (p x ↔ q x)) → filter p s = filter q s

@[simp]

theorem Multiset.filter_add {α : Type u_1} (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s + t) = filter p s + filter p t

@[simp]

theorem Multiset.filter_le {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s ≤ s

@[simp]

theorem Multiset.filter_subset {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s ⊆ s

theorem Multiset.filter_le_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s t : Multiset α} (h : s ≤ t) : filter p s ≤ filter p t

theorem Multiset.monotone_filter_left {α : Type u_1} (p : α → Prop) [DecidablePred p] : Monotone (filter p)

theorem Multiset.monotone_filter_right {α : Type u_1} (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : ∀ (b : α), p b → q b) : filter p s ≤ filter q s

@[simp]

theorem Multiset.filter_cons_of_pos {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : p a → filter p (a ::ₘ s) = a ::ₘ filter p s

@[simp]

theorem Multiset.filter_cons_of_neg {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : ¬p a → filter p (a ::ₘ s) = filter p s

@[simp]

theorem Multiset.mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : a ∈ filter p s ↔ a ∈ s ∧ p a

theorem Multiset.of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ filter p s) : p a

theorem Multiset.mem_of_mem_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : a ∈ filter p s) : a ∈ s

theorem Multiset.mem_filter_of_mem {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} {l : Multiset α} (m : a ∈ l) (h : p a) : a ∈ filter p l

@[simp]

theorem Multiset.filter_eq_self {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : filter p s = s ↔ ∀ (a : α), a ∈ s → p a

@[simp]

theorem Multiset.filter_eq_nil {α : Type u_1} {p : α → Prop} [DecidablePred p] {s : Multiset α} : filter p s = 0 ↔ ∀ (a : α), a ∈ s → ¬p a

@[simp]

theorem Multiset.filter_true {α : Type u_1} (s : Multiset α) : filter (fun (x : α) => True) s = s

@[simp]

theorem Multiset.filter_false {α : Type u_1} (s : Multiset α) : filter (fun (x : α) => False) s = 0

theorem Multiset.le_filter {α : Type u_1} {p : α → Prop} [DecidablePred p] {s t : Multiset α} : s ≤ filter p t ↔ s ≤ t ∧ ∀ (a : α), a ∈ s → p a

theorem Multiset.filter_cons {α : Type u_1} {p : α → Prop} [DecidablePred p] {a : α} (s : Multiset α) : filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

theorem Multiset.filter_singleton {α : Type u_1} {a : α} (p : α → Prop) [DecidablePred p] : filter p {a} = if p a then {a} else ∅

@[simp]

theorem Multiset.filter_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun (a : α) => p a ∧ q a) s

theorem Multiset.filter_comm {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter q (filter p s)

theorem Multiset.filter_add_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : filter p s + filter q s = filter (fun (a : α) => p a ∨ q a) s + filter (fun (a : α) => p a ∧ q a) s

theorem Multiset.filter_add_not {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : filter p s + filter (fun (a : α) => ¬p a) s = s

theorem Multiset.filter_map {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s)

theorem Multiset.map_filter {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] {f : α → β} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun (b : β) => ∃ (a : α), p a ∧ f a = b] : map f (filter p s) = filter (fun (b : β) => ∃ (a : α), p a ∧ f a = b) (map f s)

@[deprecated Multiset.map_filter (since := "2026-08-20")]

theorem Multiset.map_filter' {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] {f : α → β} (hf : Function.Injective f) (s : Multiset α) [DecidablePred fun (b : β) => ∃ (a : α), p a ∧ f a = b] : map f (filter p s) = filter (fun (b : β) => ∃ (a : α), p a ∧ f a = b) (map f s)

Alias of Multiset.map_filter.

theorem Multiset.card_filter_le_iff {α : Type u_1} (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) : (filter P s).card ≤ n ↔ ∀ (s' : Multiset α), s' ≤ s → n < s'.card → ∃ (a : α), a ∈ s' ∧ ¬P a

Simultaneously filter and map elements of a multiset

def Multiset.filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (s : Multiset α) : Multiset β

filterMap f s is a combination filter/map operation on s. The function f : α → Option β is applied to each element of s; if f a is some b then b is added to the result, otherwise a is removed from the resulting multiset.

@[simp]

theorem Multiset.filterMap_coe {α : Type u_1} {β : Type v} (f : α → Option β) (l : List α) : filterMap f ↑l = ↑(List.filterMap f l)

@[simp]

theorem Multiset.filterMap_zero {α : Type u_1} {β : Type v} (f : α → Option β) : filterMap f 0 = 0

@[simp]

theorem Multiset.filterMap_cons_none {α : Type u_1} {β : Type v} {f : α → Option β} (a : α) (s : Multiset α) (h : f a = none) : filterMap f (a ::ₘ s) = filterMap f s

@[simp]

theorem Multiset.filterMap_cons_some {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α) {b : β} (h : f a = some b) : filterMap f (a ::ₘ s) = b ::ₘ filterMap f s

theorem Multiset.filterMap_cons {α : Type u_1} {β : Type v} (f : α → Option β) (a : α) (s : Multiset α) : filterMap f (a ::ₘ s) = (Option.map singleton (f a)).getD 0 + filterMap f s

@[simp]

theorem Multiset.filterMap_add {α : Type u_1} {β : Type v} (f : α → Option β) (s t : Multiset α) : filterMap f (s + t) = filterMap f s + filterMap f t

theorem Multiset.filterMap_eq_map {α : Type u_1} {β : Type v} (f : α → β) : filterMap (some ∘ f) = map f

theorem Multiset.filterMap_eq_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] : filterMap (Option.guard fun (b : α) => decide (p b)) = filter p

theorem Multiset.filterMap_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → Option γ) (s : Multiset α) : filterMap g (filterMap f s) = filterMap (fun (x : α) => (f x).bind g) s

theorem Multiset.map_filterMap {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → γ) (s : Multiset α) : map g (filterMap f s) = filterMap (fun (x : α) => Option.map g (f x)) s

theorem Multiset.filterMap_map {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → β) (g : β → Option γ) (s : Multiset α) : filterMap g (map f s) = filterMap (g ∘ f) s

theorem Multiset.filter_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) : filter p (filterMap f s) = filterMap (fun (x : α) => Option.filter (fun (b : β) => decide (p b)) (f x)) s

theorem Multiset.filterMap_filter {α : Type u_1} {β : Type v} (p : α → Prop) [DecidablePred p] (f : α → Option β) (s : Multiset α) : filterMap f (filter p s) = filterMap (fun (x : α) => if p x then f x else none) s

@[simp]

theorem Multiset.filterMap_some {α : Type u_1} (s : Multiset α) : filterMap some s = s

@[simp]

theorem Multiset.mem_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) (s : Multiset α) {b : β} : b ∈ filterMap f s ↔ ∃ (a : α), a ∈ s ∧ f a = some b

theorem Multiset.map_filterMap_of_inv {α : Type u_1} {β : Type v} (f : α → Option β) (g : β → α) (H : ∀ (x : α), Option.map g (f x) = some x) (s : Multiset α) : map g (filterMap f s) = s

theorem Multiset.filterMap_le_filterMap {α : Type u_1} {β : Type v} (f : α → Option β) {s t : Multiset α} (h : s ≤ t) : filterMap f s ≤ filterMap f t

theorem Multiset.map_filter_eq_filterMap {α : Type u_1} {β : Type v} (f : α → β) (p : α → Prop) [DecidablePred p] (s : Multiset α) : map f (filter p s) = filterMap (fun (a : α) => if p a then some (f a) else none) s

countP

theorem Multiset.countP_eq_card_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (s : Multiset α) : countP p s = (filter p s).card

@[simp]

theorem Multiset.countP_filter {α : Type u_1} (p : α → Prop) [DecidablePred p] (q : α → Prop) [DecidablePred q] (s : Multiset α) : countP p (filter q s) = countP (fun (a : α) => p a ∧ q a) s

theorem Multiset.countP_eq_countP_filter_add {α : Type u_1} (s : Multiset α) (p q : α → Prop) [DecidablePred p] [DecidablePred q] : countP p s = countP p (filter q s) + countP p (filter (fun (a : α) => ¬q a) s)

theorem Multiset.countP_map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] : countP p (map f s) = (filter (fun (a : α) => p (f a)) s).card

theorem Multiset.filter_attach {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : filter (fun (a : { a : α // a ∈ s }) => p ↑a) s.attach = map (Subtype.map id ⋯) (filter p s).attach

Multiplicity of an element

@[simp]

theorem Multiset.count_filter_of_pos {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : p a) : count a (filter p s) = count a s

theorem Multiset.count_filter_of_neg {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} (h : ¬p a) : count a (filter p s) = 0

theorem Multiset.count_filter {α : Type u_1} [DecidableEq α] {p : α → Prop} [DecidablePred p] {a : α} {s : Multiset α} : count a (filter p s) = if p a then count a s else 0

theorem Multiset.count_map {α : Type u_3} {β : Type u_4} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) : count b (map f s) = (filter (fun (a : α) => b = f a) s).card

theorem Multiset.count_map_eq_count {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Set.InjOn f {x : α | x ∈ s}) (x : α) (H : x ∈ s) : count (f x) (map f s) = count x s

Multiset.map f preserves count if f is injective on the set of elements contained in the multiset

theorem Multiset.count_map_eq_count' {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f) (x : α) : count (f x) (map f s) = count x s

Multiset.map f preserves count if f is injective

theorem Multiset.filter_eq' {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : filter (fun (x : α) => x = b) s = replicate (count b s) b

theorem Multiset.filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (b : α) : filter (Eq b) s = replicate (count b s) b

Subtraction

@[simp]

theorem Multiset.filter_sub {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s - t) = filter p s - filter p t

@[simp]

theorem Multiset.sub_filter_eq_filter_not {α : Type u_1} [DecidableEq α] (p : α → Prop) [DecidablePred p] (s : Multiset α) : s - filter p s = filter (fun (a : α) => ¬p a) s

@[simp]

theorem Multiset.map_le_map_iff {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} : map f s ≤ map f t ↔ s ≤ t

def Multiset.mapEmbedding {α : Type u_1} {β : Type v} (f : α ↪ β) : Multiset α ↪o Multiset β

Associate to an embedding f from α to β the order embedding that maps a multiset to its image under f.

@[simp]

theorem Multiset.mapEmbedding_apply {α : Type u_1} {β : Type v} (f : α ↪ β) (s : Multiset α) : (mapEmbedding f) s = map (⇑f) s

theorem Multiset.count_eq_card_filter_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : count a s = (filter (fun (x : α) => a = x) s).card

@[simp]

theorem Multiset.map_count_True_eq_filter_card {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] [DecidableEq Prop] : count True (map p s) = (filter p s).card

Mapping a multiset through a predicate and counting the Trues yields the cardinality of the set filtered by the predicate. Note that this uses the notion of a multiset of Props - due to the decidability requirements of count, the decidability instance on the LHS is different from the RHS. In particular, the decidability instance on the left leaks Classical.decEq. See here for more discussion.

theorem Multiset.filter_attach' {α : Type u_1} (s : Multiset α) (p : { a : α // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] : filter p s.attach = map (Subtype.map id ⋯) (filter (fun (x : α) => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach

theorem Multiset.Nodup.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} : s.Nodup → (Multiset.filter p s).Nodup

theorem Multiset.Nodup.erase_eq_filter {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} : s.Nodup → s.erase a = Multiset.filter (fun (x : α) => x ≠ a) s

theorem Multiset.Nodup.filterMap {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → Option β) (H : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a') : s.Nodup → (filterMap f s).Nodup

theorem Multiset.Nodup.mem_erase_iff {α : Type u_1} [DecidableEq α] {a b : α} {l : Multiset α} (d : l.Nodup) : a ∈ l.erase b ↔ a ≠ b ∧ a ∈ l

theorem Multiset.Nodup.notMem_erase {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (h : s.Nodup) : ¬a ∈ s.erase a