Mathlib.Data.Multiset.Filter

Multiset.filter definition

(s : Multiset α) : Multiset α

Full source

/-- `Filter p s` returns the elements in `s` (with the same multiplicities)
  which satisfy `p`, and removes the rest. -/
def filter (s : Multiset α) : Multiset α :=
  Quot.liftOn s (fun l => (List.filter p l : Multiset α)) fun _l₁ _l₂ h => Quot.sound <| h.filter p

Filtering a multiset by a predicate

Informal description

Given a predicate $ p $ on elements of type $ \alpha $, the function `Multiset.filter p s` returns the multiset consisting of all elements in $ s $ that satisfy $ p $, preserving their multiplicities. Elements not satisfying $ p $ are removed.

Multiset.filter_coe theorem

(l : List α) : filter p l = l.filter p

Full source

@[simp, norm_cast] lemma filter_coe (l : List α) : filter p l = l.filter p := rfl

Equality of List and Multiset Filtering

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained by filtering $l$ with predicate $p$ is equal to the multiset formed by first converting $l$ to a multiset and then filtering it with $p$. In other words, $\text{filter}\ p\ l = l.\text{filter}\ p$.

Multiset.filter_zero theorem

: filter p 0 = 0

Full source

@[simp]
theorem filter_zero : filter p 0 = 0 :=
  rfl

Filtering the Empty Multiset Yields the Empty Multiset

Informal description

For any predicate $p$, the filter operation applied to the empty multiset $0$ yields the empty multiset, i.e., $\text{filter}\ p\ 0 = 0$.

Multiset.filter_congr theorem

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

Full source

@[congr]
theorem filter_congr {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} :
    (∀ x ∈ s, p x ↔ q x) → filter p s = filter q s :=
  Quot.inductionOn s fun _l h => congr_arg ofList <| List.filter_congr <| by simpa using h

Equality of Filtered Multisets under Equivalent Predicates

Informal description

Let $p$ and $q$ be predicates on elements of type $\alpha$, with decidable truth values. For any multiset $s$ of elements of $\alpha$, if for every element $x$ in $s$ the predicates $p(x)$ and $q(x)$ are equivalent, then the filtered multisets $\text{filter}\ p\ s$ and $\text{filter}\ q\ s$ are equal.

Multiset.filter_add theorem

(s t : Multiset α) : filter p (s + t) = filter p s + filter p t

Full source

@[simp]
theorem filter_add (s t : Multiset α) : filter p (s + t) = filter p s + filter p t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg ofList <| filter_append _ _

Filtering Preserves Multiset Addition

Informal description

For any multisets $s$ and $t$ over a type $\alpha$ and any predicate $p$ on $\alpha$, the filter of the sum $s + t$ under $p$ is equal to the sum of the filters of $s$ and $t$ under $p$, i.e., \[ \text{filter } p (s + t) = \text{filter } p s + \text{filter } p t. \]

Multiset.filter_le theorem

(s : Multiset α) : filter p s ≤ s

Full source

@[simp]
theorem filter_le (s : Multiset α) : filter p s ≤ s :=
  Quot.inductionOn s fun _l => filter_sublist.subperm

Filtered multiset is a submultiset

Informal description

For any multiset $s$ over a type $\alpha$ and any predicate $p$ on $\alpha$, the filtered multiset $\mathrm{filter}\, p\, s$ is a submultiset of $s$, i.e., $\mathrm{filter}\, p\, s \leq s$.

Multiset.filter_subset theorem

(s : Multiset α) : filter p s ⊆ s

Full source

@[simp]
theorem filter_subset (s : Multiset α) : filterfilter p s ⊆ s :=
  subset_of_le <| filter_le _ _

Filtered Multiset is a Subset of Original Multiset

Informal description

For any multiset $s$ over a type $\alpha$ and any predicate $p$ on $\alpha$, the filtered multiset $\mathrm{filter}\, p\, s$ is a subset of $s$, i.e., every element in $\mathrm{filter}\, p\, s$ appears in $s$ with at least the same multiplicity.

Multiset.filter_le_filter theorem

{s t} (h : s ≤ t) : filter p s ≤ filter p t

Full source

@[gcongr]
theorem filter_le_filter {s t} (h : s ≤ t) : filter p s ≤ filter p t :=
  leInductionOn h fun h => (h.filter (p ·)).subperm

Filter Preserves Submultiset Ordering

Informal description

For any multisets $s$ and $t$ of elements of type $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then the filtered multiset $\text{filter } p \ s$ is a submultiset of $\text{filter } p \ t$.

Multiset.monotone_filter_left theorem

: Monotone (filter p)

Full source

theorem monotone_filter_left : Monotone (filter p) := fun _s _t => filter_le_filter p

Monotonicity of Multiset Filtering with Respect to Submultiset Relation

Informal description

For any predicate $p$ on elements of type $\alpha$, the function $\mathrm{filter}\ p$ is monotone with respect to the submultiset relation $\leq$ on multisets. That is, for any multisets $s$ and $t$ of elements of type $\alpha$, if $s \leq t$, then $\mathrm{filter}\ p\ s \leq \mathrm{filter}\ p\ t$.

Multiset.monotone_filter_right theorem

 (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q] (h : ∀ b, p b → q b) : s.filter p ≤ s.filter q

Full source

theorem monotone_filter_right (s : Multiset α) ⦃p q : α → Prop⦄ [DecidablePred p] [DecidablePred q]
    (h : ∀ b, p b → q b) :
    s.filter p ≤ s.filter q :=
  Quotient.inductionOn s fun l => (l.monotone_filter_right <| by simpa using h).subperm

Monotonicity of Multiset Filtering with Respect to Predicate Implication

Informal description

For any multiset $s$ of elements of type $\alpha$ and any two predicates $p$ and $q$ on $\alpha$ such that $p(b)$ implies $q(b)$ for all $b \in \alpha$, the filtered multiset $s.\mathrm{filter}(p)$ is a submultiset of $s.\mathrm{filter}(q)$.

Multiset.filter_cons_of_pos theorem

{a : α} (s) : p a → filter p (a ::ₘ s) = a ::ₘ filter p s

Full source

@[simp]
theorem filter_cons_of_pos {a : α} (s) : p a → filter p (a ::ₘ s) = a ::ₘ filter p s :=
  Quot.inductionOn s fun _ h => congr_arg ofList <| List.filter_cons_of_pos <| by simpa using h

Filtering a Cons Multiset with Positive Predicate

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ of elements of type $\alpha$, if the predicate $p$ holds for $a$, then filtering the multiset obtained by adding $a$ to $s$ (denoted $a ::ₘ s$) with $p$ results in the multiset obtained by adding $a$ to the filtered version of $s$ (i.e., $\text{filter } p (a ::ₘ s) = a ::ₘ \text{filter } p s$).

Multiset.filter_cons_of_neg theorem

{a : α} (s) : ¬p a → filter p (a ::ₘ s) = filter p s

Full source

@[simp]
theorem filter_cons_of_neg {a : α} (s) : ¬p a → filter p (a ::ₘ s) = filter p s :=
  Quot.inductionOn s fun _ h => congr_arg ofList <| List.filter_cons_of_neg <| by simpa using h

Filtering a Multiset with a Negated Predicate on the First Element

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ of elements of type $\alpha$, if the predicate $p$ does not hold for $a$, then filtering the multiset obtained by prepending $a$ to $s$ with $p$ is equal to filtering $s$ with $p$. In symbols: \[ \text{filter } p (a \text{ ::ₘ } s) = \text{filter } p s \quad \text{when} \quad \neg p(a). \]

Multiset.mem_filter theorem

{a : α} {s} : a ∈ filter p s ↔ a ∈ s ∧ p a

Full source

@[simp]
theorem mem_filter {a : α} {s} : a ∈ filter p sa ∈ filter p s ↔ a ∈ s ∧ p a :=
  Quot.inductionOn s fun _l => by simp

Membership in Filtered Multiset Characterization

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ of elements of type $\alpha$, the element $a$ belongs to the filtered multiset $\mathrm{filter}\,p\,s$ if and only if $a$ belongs to $s$ and satisfies the predicate $p$.

Multiset.of_mem_filter theorem

{a : α} {s} (h : a ∈ filter p s) : p a

Full source

theorem of_mem_filter {a : α} {s} (h : a ∈ filter p s) : p a :=
  (mem_filter.1 h).2

Membership in Filtered Multiset Implies Predicate Holds

Informal description

For any element $a$ in a multiset $s$ and any predicate $p$, if $a$ belongs to the filtered multiset $\mathrm{filter}\,p\,s$, then $p(a)$ holds.

Multiset.mem_of_mem_filter theorem

{a : α} {s} (h : a ∈ filter p s) : a ∈ s

Full source

theorem mem_of_mem_filter {a : α} {s} (h : a ∈ filter p s) : a ∈ s :=
  (mem_filter.1 h).1

Membership in Filtered Multiset Implies Membership in Original Multiset

Informal description

For any element $a$ in a multiset $s$ and any predicate $p$, if $a$ belongs to the filtered multiset $\mathrm{filter}\,p\,s$, then $a$ belongs to $s$.

Multiset.mem_filter_of_mem theorem

{a : α} {l} (m : a ∈ l) (h : p a) : a ∈ filter p l

Full source

theorem mem_filter_of_mem {a : α} {l} (m : a ∈ l) (h : p a) : a ∈ filter p l :=
  mem_filter.2 ⟨m, h⟩

Membership Preservation in Filtered Multiset

Informal description

For any element $a$ in a multiset $l$ and any predicate $p$, if $a$ satisfies $p$, then $a$ is also in the filtered multiset $\mathrm{filter}\,p\,l$.

Multiset.filter_eq_self theorem

{s} : filter p s = s ↔ ∀ a ∈ s, p a

Full source

theorem filter_eq_self {s} : filterfilter p s = s ↔ ∀ a ∈ s, p a :=
  Quot.inductionOn s fun _l =>
    Iff.trans ⟨fun h => filter_sublist.eq_of_length (congr_arg card h),
      congr_arg ofList⟩ <| by simp

Filtered Multiset Equals Original Multiset if and only if All Elements Satisfy Predicate

Informal description

For a multiset $s$ and a predicate $p$, the filtered multiset $\mathrm{filter}\, p\, s$ is equal to $s$ if and only if every element $a$ in $s$ satisfies $p(a)$.

Multiset.filter_eq_nil theorem

{s} : filter p s = 0 ↔ ∀ a ∈ s, ¬p a

Full source

theorem filter_eq_nil {s} : filterfilter p s = 0 ↔ ∀ a ∈ s, ¬p a :=
  Quot.inductionOn s fun _l =>
    Iff.trans ⟨fun h => eq_nil_of_length_eq_zero (congr_arg card h), congr_arg ofList⟩ (by simp)

Empty Filtered Multiset Characterized by Predicate Falsity

Informal description

For a multiset $s$ and a predicate $p$, the filtered multiset $\mathrm{filter}\, p\, s$ is empty if and only if no element $a$ in $s$ satisfies $p(a)$.

Multiset.le_filter theorem

{s t} : s ≤ filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a

Full source

theorem le_filter {s t} : s ≤ filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a :=
  ⟨fun h => ⟨le_trans h (filter_le _ _), fun _a m => of_mem_filter (mem_of_le h m)⟩, fun ⟨h, al⟩ =>
    filter_eq_self.2 al ▸ filter_le_filter p h⟩

Submultiset Characterization via Filtering

Informal description

For any multisets $s$ and $t$ of elements of type $\alpha$ and any predicate $p$ on $\alpha$, the following are equivalent: 1. $s$ is a submultiset of the filtered multiset $\mathrm{filter}\, p\, t$; 2. $s$ is a submultiset of $t$ and every element $a$ in $s$ satisfies $p(a)$.

Multiset.filter_cons theorem

{a : α} (s : Multiset α) : filter p (a ::ₘ s) = (if p a then { a } else 0) + filter p s

Full source

theorem filter_cons {a : α} (s : Multiset α) :
    filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s := by
  split_ifs with h
  · rw [filter_cons_of_pos _ h, singleton_add]
  · rw [filter_cons_of_neg _ h, Multiset.zero_add]

Filtering a Cons Multiset via Predicate Branching

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ of elements of type $\alpha$, the filter of the multiset $a ::ₘ s$ with respect to predicate $p$ is equal to: - $\{a\} + \text{filter } p s$ if $p(a)$ holds - $\text{filter } p s$ otherwise (i.e., when $\neg p(a)$) where $+$ denotes multiset addition.

Multiset.filter_singleton theorem

{a : α} (p : α → Prop) [DecidablePred p] : filter p { a } = if p a then { a } else ∅

Full source

theorem filter_singleton {a : α} (p : α → Prop) [DecidablePred p] :
    filter p {a} = if p a then {a} else ∅ := by
  simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

Filtering a Singleton Multiset via Predicate Branching

Informal description

For any element $a$ of type $\alpha$ and any decidable predicate $p$ on $\alpha$, the filtered multiset $\text{filter } p \{a\}$ equals $\{a\}$ if $p(a)$ holds, and the empty multiset $\emptyset$ otherwise.

Multiset.filter_filter theorem

(q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter (fun a => p a ∧ q a) s

Full source

@[simp]
theorem filter_filter (q) [DecidablePred q] (s : Multiset α) :
    filter p (filter q s) = filter (fun a => p a ∧ q a) s :=
  Quot.inductionOn s fun l => by simp

Composition of Multiset Filters via Conjunction

Informal description

For any decidable predicates $ p $ and $ q $ on elements of type $ \alpha $, and for any multiset $ s $ of elements in $ \alpha $, the result of filtering $ s $ first by $ q $ and then by $ p $ is equal to filtering $ s $ by the conjunction $ \lambda a, p(a) \land q(a) $. In other words: \[ \text{filter } p (\text{filter } q s) = \text{filter } (a \mapsto p(a) \land q(a)) s \]

Multiset.filter_comm theorem

(q) [DecidablePred q] (s : Multiset α) : filter p (filter q s) = filter q (filter p s)

Full source

lemma filter_comm (q) [DecidablePred q] (s : Multiset α) :
    filter p (filter q s) = filter q (filter p s) := by simp [and_comm]

Commutativity of Multiset Filtering

Informal description

For any decidable predicates $p$ and $q$ on elements of type $\alpha$, and for any multiset $s$ of elements in $\alpha$, the order of filtering $s$ by $p$ and $q$ does not affect the result. That is: \[ \text{filter } p (\text{filter } q s) = \text{filter } q (\text{filter } p s) \]

Multiset.filter_add_filter theorem

 (q) [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

Full source

theorem filter_add_filter (q) [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 :=
  Multiset.induction_on s rfl fun a s IH => by by_cases p a <;> by_cases q a <;> simp [*]

Decomposition of Filtered Multiset Sum via Disjunction and Conjunction

Informal description

For any decidable predicates $p$ and $q$ on elements of type $\alpha$, and for any multiset $s$ of elements in $\alpha$, the sum of the multisets obtained by filtering $s$ with $p$ and $q$ respectively is equal to the sum of the multisets obtained by filtering $s$ with the disjunction $p \lor q$ and the conjunction $p \land q$. In symbols: \[ \text{filter } p\ s + \text{filter } q\ s = \text{filter } (a \mapsto p(a) \lor q(a))\ s + \text{filter } (a \mapsto p(a) \land q(a))\ s. \]

Multiset.filter_add_not theorem

(s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s

Full source

theorem filter_add_not (s : Multiset α) : filter p s + filter (fun a => ¬p a) s = s := by
  rw [filter_add_filter, filter_eq_self.2, filter_eq_nil.2]
  · simp only [Multiset.add_zero]
  · simp [Decidable.em, -Bool.not_eq_true, -not_and, not_and_or, or_comm]
  · simp only [Bool.not_eq_true, decide_eq_true_eq, Bool.eq_false_or_eq_true,
      decide_true, implies_true, Decidable.em]

Decomposition of a Multiset into Filtered Parts: $s = \text{filter } p\ s + \text{filter } (\neg p)\ s$

Informal description

For any multiset $s$ of elements of type $\alpha$ and any predicate $p$ on $\alpha$, the sum of the multisets obtained by filtering $s$ with $p$ and its negation $\neg p$ equals $s$. That is, \[ \text{filter } p\ s + \text{filter } (\neg p)\ s = s. \]

Multiset.filter_map theorem

(f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s)

Full source

theorem filter_map (f : β → α) (s : Multiset β) : filter p (map f s) = map f (filter (p ∘ f) s) :=
  Quot.inductionOn s fun l => by simp [List.filter_map]; rfl

Filter-Map Commutation for Multisets: $\text{filter}\ p \circ \text{map}\ f = \text{map}\ f \circ \text{filter}\ (p \circ f)$

Informal description

Let $f : \beta \to \alpha$ be a function and $s$ a multiset of elements of type $\beta$. Then filtering the mapped multiset $\text{map}\ f\ s$ by a predicate $p$ is equivalent to first filtering $s$ by the predicate $p \circ f$ and then applying $f$ to the result. That is, \[ \text{filter}\ p\ (\text{map}\ f\ s) = \text{map}\ f\ (\text{filter}\ (p \circ f)\ s). \]

Multiset.map_filter' theorem

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

Full source

lemma map_filter' {f : α → β} (hf : Injective f) (s : Multiset α)
    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
    (s.filter p).map f = (s.map f).filter fun b => ∃ a, p a ∧ f a = b := by
  simp [comp_def, filter_map, hf.eq_iff]

Filter-Map Commutation for Injective Functions on Multisets

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s$ a multiset of elements of type $\alpha$. Suppose the predicate $\exists a, p(a) \land f(a) = b$ is decidable for any $b \in \beta$. Then the image under $f$ of the filtered multiset $\mathrm{filter}\, p\, s$ is equal to the filtered image of $s$ under $f$, where the filter condition is that there exists an element $a$ in the original multiset such that $p(a)$ holds and $f(a) = b$. That is, \[ \mathrm{map}\, f\, (\mathrm{filter}\, p\, s) = \mathrm{filter}\, (\lambda b, \exists a, p(a) \land f(a) = b)\, (\mathrm{map}\, f\, s). \]

Multiset.card_filter_le_iff theorem

 (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
  card (s.filter P) ≤ n ↔ ∀ s' ≤ s, n < card s' → ∃ a ∈ s', ¬P a

Full source

lemma card_filter_le_iff (s : Multiset α) (P : α → Prop) [DecidablePred P] (n : ℕ) :
    cardcard (s.filter P) ≤ n ↔ ∀ s' ≤ s, n < card s' → ∃ a ∈ s', ¬ P a := by
  fconstructor
  · intro H s' hs' s'_card
    by_contra! rid
    have card := card_le_card (monotone_filter_left P hs') |>.trans H
    exact s'_card.not_le (filter_eq_self.mpr rid ▸ card)
  · contrapose!
    exact fun H ↦ ⟨s.filter P, filter_le _ _, H, fun a ha ↦ (mem_filter.mp ha).2⟩

Cardinality Bound of Filtered Multiset via Submultisets

Informal description

For a multiset $s$ of elements of type $\alpha$, a predicate $P$ on $\alpha$, and a natural number $n$, the cardinality of the filtered multiset $\mathrm{filter}\, P\, s$ is at most $n$ if and only if for every submultiset $s'$ of $s$ with cardinality greater than $n$, there exists an element $a \in s'$ that does not satisfy $P$.

Multiset.filterMap definition

(f : α → Option β) (s : Multiset α) : Multiset β

Full source

/-- `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. -/
def filterMap (f : α → Option β) (s : Multiset α) : Multiset β :=
  Quot.liftOn s (fun l => (List.filterMap f l : Multiset β))
    fun _l₁ _l₂ h => Quot.sound <| h.filterMap f

Filter and map operation on multisets

Informal description

Given a function $ f : \alpha \to \text{Option } \beta $ and a multiset $ s $ of elements of type $ \alpha $, the operation `filterMap` constructs a new multiset of elements of type $ \beta $ by applying $ f $ to each element of $ s $. If $ f(a) = \text{some } b $ for an element $ a \in s $, then $ b $ is included in the resulting multiset; otherwise, the element is excluded.

Multiset.filterMap_coe theorem

(f : α → Option β) (l : List α) : filterMap f l = l.filterMap f

Full source

@[simp, norm_cast]
lemma filterMap_coe (f : α → Option β) (l : List α) : filterMap f l = l.filterMap f := rfl

Equivalence of `filterMap` between List and Multiset Representations

Informal description

Given a function $f : \alpha \to \text{Option } \beta$ and a list $l$ of elements of type $\alpha$, the multiset obtained by applying `filterMap f` to the multiset version of $l$ is equal to the multiset version of the list obtained by applying `List.filterMap f` to $l$.

Multiset.filterMap_zero theorem

(f : α → Option β) : filterMap f 0 = 0

Full source

@[simp]
theorem filterMap_zero (f : α → Option β) : filterMap f 0 = 0 :=
  rfl

FilterMap of Empty Multiset is Empty

Informal description

For any function $f : \alpha \to \text{Option } \beta$, applying the `filterMap` operation to the empty multiset $0$ results in the empty multiset, i.e., $\text{filterMap } f \, 0 = 0$.

Multiset.filterMap_cons_none theorem

{f : α → Option β} (a : α) (s : Multiset α) (h : f a = none) : filterMap f (a ::ₘ s) = filterMap f s

Full source

@[simp]
theorem filterMap_cons_none {f : α → Option β} (a : α) (s : Multiset α) (h : f a = none) :
    filterMap f (a ::ₘ s) = filterMap f s :=
  Quot.inductionOn s fun _ => congr_arg ofList <| List.filterMap_cons_none h

Filter-map operation preserves structure when function evaluates to none

Informal description

Let $f : \alpha \to \text{Option } \beta$ be a function, $a \in \alpha$ an element, and $s$ a multiset of elements of type $\alpha$. If $f(a) = \text{none}$, then the filter-map operation satisfies $\text{filterMap } f (a \cup s) = \text{filterMap } f s$, where $\cup$ denotes multiset cons operation.

Multiset.filterMap_cons_some theorem

 (f : α → Option β) (a : α) (s : Multiset α) {b : β} (h : f a = some b) : filterMap f (a ::ₘ s) = b ::ₘ filterMap f s

Full source

@[simp]
theorem filterMap_cons_some (f : α → Option β) (a : α) (s : Multiset α) {b : β}
    (h : f a = some b) : filterMap f (a ::ₘ s) = b ::ₘ filterMap f s :=
  Quot.inductionOn s fun _ => congr_arg ofList <| List.filterMap_cons_some h

Filter-and-map operation with some result preserves multiset union

Informal description

Given a function $f : \alpha \to \text{Option } \beta$, an element $a \in \alpha$, a multiset $s$ of elements of type $\alpha$, and an element $b \in \beta$ such that $f(a) = \text{some } b$, the filter-and-map operation satisfies: \[ \text{filterMap } f (a \cup s) = b \cup \text{filterMap } f s \] where $\cup$ denotes multiset union.

Multiset.filterMap_eq_map theorem

(f : α → β) : filterMap (some ∘ f) = map f

Full source

theorem filterMap_eq_map (f : α → β) : filterMap (somesome ∘ f) = map f :=
  funext fun s =>
    Quot.inductionOn s fun l => congr_arg ofList <| congr_fun List.filterMap_eq_map l

Equivalence of `filterMap` and `map` for total functions

Informal description

For any function $f : \alpha \to \beta$, the operation `filterMap` applied with the composition of `some` and $f$ is equivalent to the `map` operation with $f$. In other words, $\text{filterMap}\, (\text{some} \circ f) = \text{map}\, f$.

Multiset.filterMap_eq_filter theorem

: filterMap (Option.guard p) = filter p

Full source

theorem filterMap_eq_filter : filterMap (Option.guard p) = filter p :=
  funext fun s =>
    Quot.inductionOn s fun l => congr_arg ofList <| by
      rw [← List.filterMap_eq_filter]
      congr; funext a; simp

Equivalence of Filtering via `filterMap` and `filter`

Informal description

For any predicate $p$, the operation `filterMap` with the function `Option.guard p` is equivalent to the `filter p` operation on multisets. That is, $\text{filterMap}\, (\text{Option.guard}\, p) = \text{filter}\, p$.

Multiset.filterMap_filterMap theorem

 (f : α → Option β) (g : β → Option γ) (s : Multiset α) :
  filterMap g (filterMap f s) = filterMap (fun x => (f x).bind g) s

Full source

theorem filterMap_filterMap (f : α → Option β) (g : β → Option γ) (s : Multiset α) :
    filterMap g (filterMap f s) = filterMap (fun x => (f x).bind g) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_filterMap

Composition Law for Filter-Mapping Multisets: $g \circ_{\text{filter}} f = f \bind g$

Informal description

For any function $f : \alpha \to \text{Option } \beta$, any function $g : \beta \to \text{Option } \gamma$, and any multiset $s$ of elements of type $\alpha$, the composition of filter-mapping with $g$ after filter-mapping with $f$ is equal to filter-mapping with the composition $\lambda x, (f x) \bind g$.

Multiset.map_filterMap theorem

(f : α → Option β) (g : β → γ) (s : Multiset α) : map g (filterMap f s) = filterMap (fun x => (f x).map g) s

Full source

theorem map_filterMap (f : α → Option β) (g : β → γ) (s : Multiset α) :
    map g (filterMap f s) = filterMap (fun x => (f x).map g) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.map_filterMap

Commutativity of Map and FilterMap on Multisets: $\text{map } g \circ \text{filterMap } f = \text{filterMap } (f \circ \text{map } g)$

Informal description

Given a function $f : \alpha \to \text{Option } \beta$, a function $g : \beta \to \gamma$, and a multiset $s$ of elements of type $\alpha$, the map of $g$ over the filterMap of $f$ on $s$ is equal to the filterMap of the composition $(f x).\text{map } g$ on $s$. In symbols: \[ \text{map } g (\text{filterMap } f \, s) = \text{filterMap } (\lambda x, (f x).\text{map } g) \, s \]

Multiset.filterMap_map theorem

(f : α → β) (g : β → Option γ) (s : Multiset α) : filterMap g (map f s) = filterMap (g ∘ f) s

Full source

theorem filterMap_map (f : α → β) (g : β → Option γ) (s : Multiset α) :
    filterMap g (map f s) = filterMap (g ∘ f) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_map

Commutativity of FilterMap and Map Operations on Multisets

Informal description

For any function $f : \alpha \to \beta$, a function $g : \beta \to \text{Option } \gamma$, and a multiset $s$ of elements of type $\alpha$, the following equality holds: \[ \text{filterMap } g (\text{map } f s) = \text{filterMap } (g \circ f) s. \] Here, $\text{filterMap } h t$ denotes the multiset obtained by applying $h$ to each element of $t$ and collecting all $\text{some } y$ results, while $\text{map } f s$ is the multiset obtained by applying $f$ to each element of $s$.

Multiset.filter_filterMap theorem

 (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) :
  filter p (filterMap f s) = filterMap (fun x => (f x).filter p) s

Full source

theorem filter_filterMap (f : α → Option β) (p : β → Prop) [DecidablePred p] (s : Multiset α) :
    filter p (filterMap f s) = filterMap (fun x => (f x).filter p) s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filter_filterMap

Commutativity of Filtering and Filter-Mapping on Multisets

Informal description

Given a function $f : \alpha \to \text{Option } \beta$, a predicate $p$ on $\beta$, and a multiset $s$ of elements of type $\alpha$, the multiset obtained by first applying `filterMap f` to $s$ and then filtering the result by $p$ is equal to the multiset obtained by applying `filterMap` with the function $\lambda x, (f x).\text{filter } p$ to $s$.

Multiset.filterMap_filter theorem

(f : α → Option β) (s : Multiset α) : filterMap f (filter p s) = filterMap (fun x => if p x then f x else none) s

Full source

theorem filterMap_filter (f : α → Option β) (s : Multiset α) :
    filterMap f (filter p s) = filterMap (fun x => if p x then f x else none) s :=
  Quot.inductionOn s fun l => congr_arg ofList <| by
    simpa using List.filterMap_filter (f := f) (p := p)

Commutativity of Filter and FilterMap Operations on Multisets

Informal description

Given a function $f : \alpha \to \text{Option } \beta$, a predicate $p : \alpha \to \text{Prop}$, and a multiset $s$ of elements of type $\alpha$, the operation of first filtering $s$ by $p$ and then applying `filterMap` with $f$ is equivalent to applying `filterMap` with a function that conditionally applies $f$ based on $p$. That is, \[ \text{filterMap } f (\text{filter } p s) = \text{filterMap } (\lambda x, \text{if } p x \text{ then } f x \text{ else none}) s. \]

Multiset.filterMap_some theorem

(s : Multiset α) : filterMap some s = s

Full source

@[simp]
theorem filterMap_some (s : Multiset α) : filterMap some s = s :=
  Quot.inductionOn s fun _ => congr_arg ofList List.filterMap_some

Identity Property of `filterMap` with `some`: $\text{filterMap}(\text{some}, s) = s$

Informal description

For any multiset $s$ of elements of type $\alpha$, applying the `filterMap` operation with the identity function `some` (which wraps each element in `Option`) returns the original multiset $s$.

Multiset.mem_filterMap theorem

(f : α → Option β) (s : Multiset α) {b : β} : b ∈ filterMap f s ↔ ∃ a, a ∈ s ∧ f a = some b

Full source

@[simp]
theorem mem_filterMap (f : α → Option β) (s : Multiset α) {b : β} :
    b ∈ filterMap f sb ∈ filterMap f s ↔ ∃ a, a ∈ s ∧ f a = some b :=
  Quot.inductionOn s fun _ => List.mem_filterMap

Membership in Filtered Multiset via Option-valued Function

Informal description

For a function $f : \alpha \to \text{Option } \beta$, a multiset $s$ of elements of type $\alpha$, and an element $b : \beta$, we have that $b$ is in the filtered multiset $\text{filterMap } f \ s$ if and only if there exists an element $a \in s$ such that $f(a) = \text{some } b$.

Multiset.map_filterMap_of_inv theorem

 (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x) (s : Multiset α) : map g (filterMap f s) = s

Full source

theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
    (s : Multiset α) : map g (filterMap f s) = s :=
  Quot.inductionOn s fun _ => congr_arg ofList <| List.map_filterMap_of_inv H

Recovery of Original Multiset via FilterMap and Inverse Map

Informal description

Let $f : \alpha \to \text{Option } \beta$ and $g : \beta \to \alpha$ be functions such that for every $x \in \alpha$, we have $(f x).\text{map } g = \text{some } x$. Then for any multiset $s$ of elements of type $\alpha$, applying the map $g$ to the filtered multiset $\text{filterMap } f s$ recovers the original multiset $s$, i.e., $\text{map } g (\text{filterMap } f s) = s$.

Multiset.filterMap_le_filterMap theorem

(f : α → Option β) {s t : Multiset α} (h : s ≤ t) : filterMap f s ≤ filterMap f t

Full source

@[gcongr]
theorem filterMap_le_filterMap (f : α → Option β) {s t : Multiset α} (h : s ≤ t) :
    filterMap f s ≤ filterMap f t :=
  leInductionOn h fun h => (h.filterMap _).subperm

Monotonicity of Filter-Map Operation on Multisets

Informal description

For any function $f : \alpha \to \text{Option } \beta$ and multisets $s, t$ of elements of type $\alpha$, if $s$ is a submultiset of $t$ (denoted $s \leq t$), then the filtered and mapped multiset $\text{filterMap } f\ s$ is a submultiset of $\text{filterMap } f\ t$.

Multiset.countP_eq_card_filter theorem

(s) : countP p s = card (filter p s)

Full source

theorem countP_eq_card_filter (s) : countP p s = card (filter p s) :=
  Quot.inductionOn s fun l => l.countP_eq_length_filter (p := (p ·))

Count of Predicate-Satisfying Elements Equals Filtered Multiset Cardinality

Informal description

For any multiset $s$ and predicate $p$, the count of elements in $s$ satisfying $p$ is equal to the cardinality of the filtered multiset $\text{filter } p \ s$. That is, $\text{countP } p \ s = \text{card } (\text{filter } p \ s)$.

Multiset.countP_filter theorem

(q) [DecidablePred q] (s : Multiset α) : countP p (filter q s) = countP (fun a => p a ∧ q a) s

Full source

@[simp]
theorem countP_filter (q) [DecidablePred q] (s : Multiset α) :
    countP p (filter q s) = countP (fun a => p a ∧ q a) s := by simp [countP_eq_card_filter]

Count of Predicate in Filtered Multiset Equals Count of Conjunction

Informal description

For any decidable predicates $p$ and $q$ on elements of type $\alpha$, and for any multiset $s$ of elements in $\alpha$, the count of elements satisfying $p$ in the filtered multiset $\text{filter } q \ s$ is equal to the count of elements satisfying the conjunction $\lambda a, p(a) \land q(a)$ in $s$. That is, \[ \text{countP } p (\text{filter } q \ s) = \text{countP } (a \mapsto p(a) \land q(a)) \ s. \]

Multiset.countP_eq_countP_filter_add theorem

 (s) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
  countP p s = (filter q s).countP p + (filter (fun a => ¬q a) s).countP p

Full source

theorem countP_eq_countP_filter_add (s) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    countP p s = (filter q s).countP p + (filter (fun a => ¬q a) s).countP p :=
  Quot.inductionOn s fun l => by
    convert l.countP_eq_countP_filter_add (p ·) (q ·)
    simp [countP_filter]

Additivity of Count over Filtered Multisets: $\text{countP}_p(s) = \text{countP}_p(\text{filter}_q(s)) + \text{countP}_p(\text{filter}_{\neg q}(s))$

Informal description

For any multiset $s$ over a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the count of elements satisfying $p$ in $s$ equals the sum of counts of elements satisfying $p$ in the filtered multisets $s$ by $q$ and $s$ by $\neg q$. That is, \[ \text{countP}_p(s) = \text{countP}_p(\text{filter}_q(s)) + \text{countP}_p(\text{filter}_{\neg q}(s)). \]

Multiset.countP_map theorem

 (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] : countP p (map f s) = card (s.filter fun a => p (f a))

Full source

theorem countP_map (f : α → β) (s : Multiset α) (p : β → Prop) [DecidablePred p] :
    countP p (map f s) = card (s.filter fun a => p (f a)) := by
  refine Multiset.induction_on s ?_ fun a t IH => ?_
  · rw [map_zero, countP_zero, filter_zero, card_zero]
  · rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

Count of Predicate in Mapped Multiset Equals Cardinality of Pre-Filtered Multiset

Informal description

For any function $f \colon \alpha \to \beta$, multiset $s$ over $\alpha$, and decidable predicate $p$ on $\beta$, the count of elements in the mapped multiset $\text{map}\, f\, s$ that satisfy $p$ is equal to the cardinality of the filtered multiset $\text{filter}\, (a \mapsto p(f(a)))\, s$. That is, \[ \text{countP}_p(\text{map}\, f\, s) = \text{card}\, (\text{filter}\, (a \mapsto p(f(a)))\, s). \]

Multiset.filter_attach theorem

 (s : Multiset α) (p : α → Prop) [DecidablePred p] :
  (s.attach.filter fun a : { a // a ∈ s } ↦ p ↑a) =
    (s.filter p).attach.map (Subtype.map id fun _ ↦ Multiset.mem_of_mem_filter)

Full source

lemma filter_attach (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    (s.attach.filter fun a : {a // a ∈ s} ↦ p ↑a) =
      (s.filter p).attach.map (Subtype.map id fun _ ↦ Multiset.mem_of_mem_filter) :=
  Quotient.inductionOn s fun l ↦ congr_arg _ (List.filter_attach l p)

Equivalence of Filtered Attached Multiset and Mapped Attached Filtered Multiset

Informal description

For any multiset $s$ over a type $\alpha$ and a decidable predicate $p$ on $\alpha$, the filtered multiset of the attached multiset (where each element is paired with a proof of its membership in $s$) under $p$ is equal to the attached multiset of the filtered multiset $s$ under $p$, mapped via the inclusion function that preserves membership proofs. More precisely, let $\text{attach}(s) = \{(a, h) \mid a \in s, h : a \in s\}$ be the multiset of pairs where each element $a$ is paired with a proof $h$ of its membership in $s$. Then: \[ \text{filter}\, p\, (\text{attach}(s)) = \text{map}\, (\text{Subtype.map}\, \text{id}\, (\lambda \_, \text{mem\_of\_mem\_filter}))\, (\text{attach}(\text{filter}\, p\, s)), \] where $\text{Subtype.map}\, \text{id}\, (\lambda \_, \text{mem\_of\_mem\_filter})$ is the function that maps an element $(a, h)$ of $\text{attach}(\text{filter}\, p\, s)$ to $(a, h')$, where $h'$ is a proof that $a \in s$ derived from $h : a \in \text{filter}\, p\, s$.

Multiset.count_filter_of_pos theorem

{p} [DecidablePred p] {a} {s : Multiset α} (h : p a) : count a (filter p s) = count a s

Full source

@[simp]
theorem count_filter_of_pos {p} [DecidablePred p] {a} {s : Multiset α} (h : p a) :
    count a (filter p s) = count a s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', filter_coe, mem_coe, coe_count, decide_eq_true_eq]
    apply count_filter
    simpa using h

Preservation of Count in Filtered Multiset for Satisfying Elements

Informal description

Let $p$ be a decidable predicate on elements of type $\alpha$, $a$ an element of $\alpha$, and $s$ a multiset of $\alpha$. If $p(a)$ holds, then the multiplicity of $a$ in the filtered multiset $\mathrm{filter}\, p\, s$ equals the multiplicity of $a$ in $s$, i.e., $\mathrm{count}\, a\, (\mathrm{filter}\, p\, s) = \mathrm{count}\, a\, s$.

Multiset.count_filter_of_neg theorem

{p} [DecidablePred p] {a} {s : Multiset α} (h : ¬p a) : count a (filter p s) = 0

Full source

@[simp]
theorem count_filter_of_neg {p} [DecidablePred p] {a} {s : Multiset α} (h : ¬p a) :
    count a (filter p s) = 0 :=
  Multiset.count_eq_zero_of_not_mem fun t => h (of_mem_filter t)

Zero Count in Filtered Multiset for Non-Satisfying Elements

Informal description

For any decidable predicate $p$ on elements of type $\alpha$, any element $a \in \alpha$, and any multiset $s$ over $\alpha$, if $a$ does not satisfy $p$ (i.e., $\neg p(a)$), then the multiplicity of $a$ in the filtered multiset $\mathrm{filter}\, p\, s$ is zero, i.e., $\mathrm{count}\, a\, (\mathrm{filter}\, p\, s) = 0$.

Multiset.count_filter theorem

{p} [DecidablePred p] {a} {s : Multiset α} : count a (filter p s) = if p a then count a s else 0

Full source

theorem count_filter {p} [DecidablePred p] {a} {s : Multiset α} :
    count a (filter p s) = if p a then count a s else 0 := by
  split_ifs with h
  · exact count_filter_of_pos h
  · exact count_filter_of_neg h

Count in Filtered Multiset Equals Count if Satisfying, Zero Otherwise

Informal description

For any decidable predicate $p$ on elements of type $\alpha$, any element $a \in \alpha$, and any multiset $s$ over $\alpha$, the multiplicity of $a$ in the filtered multiset $\mathrm{filter}\, p\, s$ is equal to the multiplicity of $a$ in $s$ if $p(a)$ holds, and zero otherwise. That is, \[ \mathrm{count}\, a\, (\mathrm{filter}\, p\, s) = \begin{cases} \mathrm{count}\, a\, s & \text{if } p(a), \\ 0 & \text{otherwise.} \end{cases} \]

Multiset.count_map theorem

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

Full source

theorem count_map {α β : Type*} (f : α → β) (s : Multiset α) [DecidableEq β] (b : β) :
    count b (map f s) = card (s.filter fun a => b = f a) := by
  simp [Bool.beq_eq_decide_eq, eq_comm, count, countP_map]

Count in Mapped Multiset Equals Cardinality of Preimage Filter

Informal description

For any function $f \colon \alpha \to \beta$, multiset $s$ over $\alpha$, and decidable equality on $\beta$, the count of an element $b \in \beta$ in the mapped multiset $\mathrm{map}\, f\, s$ is equal to the cardinality of the filtered multiset $\mathrm{filter}\, (a \mapsto b = f(a))\, s$. That is, \[ \mathrm{count}\, b\, (\mathrm{map}\, f\, s) = \mathrm{card}\, \{a \in s \mid b = f(a)\}. \]

Multiset.count_map_eq_count theorem

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

Full source

/-- `Multiset.map f` preserves `count` if `f` is injective on the set of elements contained in
the multiset -/
theorem count_map_eq_count [DecidableEq β] (f : α → β) (s : Multiset α)
    (hf : Set.InjOn f { x : α | x ∈ s }) (x) (H : x ∈ s) : (s.map f).count (f x) = s.count x := by
  suffices (filter (fun a : α => f x = f a) s).count x = card (filter (fun a : α => f x = f a) s) by
    rw [count, countP_map, ← this]
    exact count_filter_of_pos <| rfl
  · rw [eq_replicate_card.2 fun b hb => (hf H (mem_filter.1 hb).left _).symm]
    · simp only [count_replicate, eq_self_iff_true, if_true, card_replicate]
    · simp only [mem_filter, beq_iff_eq, and_imp, @eq_comm _ (f x), imp_self, implies_true]

Preservation of Count under Injective Mapping on Multiset Elements

Informal description

Let $f \colon \alpha \to \beta$ be a function, $s$ a multiset over $\alpha$, and suppose $f$ is injective on the set of elements in $s$. Then for any element $x \in s$, the multiplicity of $f(x)$ in the mapped multiset $\mathrm{map}\, f\, s$ equals the multiplicity of $x$ in $s$, i.e., \[ \mathrm{count}\, (f(x))\, (\mathrm{map}\, f\, s) = \mathrm{count}\, x\, s. \]

Multiset.count_map_eq_count' theorem

 [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f) (x : α) : (s.map f).count (f x) = s.count x

Full source

/-- `Multiset.map f` preserves `count` if `f` is injective -/
theorem count_map_eq_count' [DecidableEq β] (f : α → β) (s : Multiset α) (hf : Function.Injective f)
    (x : α) : (s.map f).count (f x) = s.count x := by
  by_cases H : x ∈ s
  · exact count_map_eq_count f _ hf.injOn _ H
  · rw [count_eq_zero_of_not_mem H, count_eq_zero, mem_map]
    rintro ⟨k, hks, hkx⟩
    rw [hf hkx] at hks
    contradiction

Preservation of Count under Injective Mapping on Multisets

Informal description

Let $f \colon \alpha \to \beta$ be an injective function and $s$ a multiset over $\alpha$. Then for any element $x \in \alpha$, the multiplicity of $f(x)$ in the mapped multiset $\mathrm{map}\, f\, s$ equals the multiplicity of $x$ in $s$, i.e., \[ \mathrm{count}\, (f(x))\, (\mathrm{map}\, f\, s) = \mathrm{count}\, x\, s. \]

Multiset.filter_eq' theorem

(s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b

Full source

theorem filter_eq' (s : Multiset α) (b : α) : s.filter (· = b) = replicate (count b s) b :=
  Quotient.inductionOn s fun l => by
    simp only [quot_mk_to_coe, filter_coe, mem_coe, coe_count]
    rw [List.filter_eq, coe_replicate]

Filtering a Multiset by Equality to an Element Yields Replicated Copies

Informal description

For any multiset $s$ of elements of type $\alpha$ and any element $b \in \alpha$, the multiset obtained by filtering $s$ to keep only elements equal to $b$ is equal to the multiset consisting of $n$ copies of $b$, where $n$ is the count of $b$ in $s$. In symbols: $$ \text{filter } (\lambda x \Rightarrow x = b) \ s = \text{replicate } (\text{count } b \ s) \ b $$

Multiset.filter_eq theorem

(s : Multiset α) (b : α) : s.filter (Eq b) = replicate (count b s) b

Full source

theorem filter_eq (s : Multiset α) (b : α) : s.filter (Eq b) = replicate (count b s) b := by
  simp_rw [← filter_eq', eq_comm]

Filtering by Equality Yields Replicated Copies

Informal description

For any multiset $s$ of elements of type $\alpha$ and any element $b \in \alpha$, the multiset obtained by filtering $s$ to keep only elements equal to $b$ is equal to the multiset consisting of $\text{count}(b, s)$ copies of $b$. In symbols: $$ \text{filter } (x \mapsto x = b) \ s = \text{replicate } (\text{count } b \ s) \ b $$

Multiset.filter_sub theorem

(p : α → Prop) [DecidablePred p] (s t : Multiset α) : filter p (s - t) = filter p s - filter p t

Full source

@[simp]
lemma filter_sub (p : α → Prop) [DecidablePred p] (s t : Multiset α) :
    filter p (s - t) = filter p s - filter p t := by
  revert s; refine Multiset.induction_on t (by simp) fun a t IH s => ?_
  rw [sub_cons, IH]
  by_cases h : p a
  · rw [filter_cons_of_pos _ h, sub_cons]
    congr
    by_cases m : a ∈ s
    · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
    · rw [erase_of_not_mem m, erase_of_not_mem (mt mem_of_mem_filter m)]
  · rw [filter_cons_of_neg _ h]
    by_cases m : a ∈ s
    · rw [(by rw [filter_cons_of_neg _ h] : filter p (erase s a) = filter p (a ::ₘ erase s a)),
        cons_erase m]
    · rw [erase_of_not_mem m]

Filtering Preserves Multiset Difference: $\mathrm{filter}\, p\, (s - t) = \mathrm{filter}\, p\, s - \mathrm{filter}\, p\, t$

Informal description

For any decidable predicate $p$ on elements of type $\alpha$ and any multisets $s$ and $t$ of elements of type $\alpha$, the multiset obtained by filtering the difference $s - t$ with $p$ is equal to the difference of the filtered multisets $\mathrm{filter}\, p\, s$ and $\mathrm{filter}\, p\, t$. In symbols: \[ \mathrm{filter}\, p\, (s - t) = \mathrm{filter}\, p\, s - \mathrm{filter}\, p\, t \]

Multiset.sub_filter_eq_filter_not theorem

(p : α → Prop) [DecidablePred p] (s : Multiset α) : s - s.filter p = s.filter fun a ↦ ¬p a

Full source

@[simp]
lemma sub_filter_eq_filter_not (p : α → Prop) [DecidablePred p] (s : Multiset α) :
    s - s.filter p = s.filter fun a ↦ ¬ p a := by ext a; by_cases h : p a <;> simp [h]

Difference of Multiset and Filter Equals Filter of Negated Predicate

Informal description

For any decidable predicate $p$ on elements of type $\alpha$ and any multiset $s$ of $\alpha$, the difference between $s$ and the filtered multiset $\mathrm{filter}\, p\, s$ equals the multiset obtained by filtering $s$ with the negated predicate $\lambda a, \neg p(a)$. In symbols: $$ s - \mathrm{filter}\, p\, s = \mathrm{filter}\, (\lambda a, \neg p(a))\, s $$

Multiset.map_le_map_iff theorem

{f : α → β} (hf : Function.Injective f) {s t : Multiset α} : s.map f ≤ t.map f ↔ s ≤ t

Full source

@[simp]
theorem map_le_map_iff {f : α → β} (hf : Function.Injective f) {s t : Multiset α} :
    s.map f ≤ t.map f ↔ s ≤ t := by
  classical
    refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
    simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

Order Preservation under Injective Mapping of Multisets: $\mathrm{map}\, f\, s \leq \mathrm{map}\, f\, t \leftrightarrow s \leq t$

Informal description

Let $f \colon \alpha \to \beta$ be an injective function, and let $s$ and $t$ be multisets over $\alpha$. Then the image of $s$ under $f$ is less than or equal to the image of $t$ under $f$ if and only if $s$ is less than or equal to $t$. In symbols: \[ \mathrm{map}\, f\, s \leq \mathrm{map}\, f\, t \leftrightarrow s \leq t. \]

Multiset.mapEmbedding definition

(f : α ↪ β) : Multiset α ↪o Multiset β

Full source

/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a multiset to its
image under `f`. -/
@[simps!]
def mapEmbedding (f : α ↪ β) : MultisetMultiset α ↪o Multiset β :=
  OrderEmbedding.ofMapLEIff (map f) fun _ _ => map_le_map_iff f.inj'

Order embedding of multisets induced by an embedding

Informal description

Given an embedding $f$ from a type $\alpha$ to a type $\beta$, the function maps a multiset $s$ over $\alpha$ to its image under $f$ as a multiset over $\beta$, and this mapping is an order embedding. That is, for any multisets $s$ and $t$ over $\alpha$, $s \leq t$ if and only if $f(s) \leq f(t)$.

Multiset.count_eq_card_filter_eq theorem

[DecidableEq α] (s : Multiset α) (a : α) : s.count a = card (s.filter (a = ·))

Full source

theorem count_eq_card_filter_eq [DecidableEq α] (s : Multiset α) (a : α) :
    s.count a = card (s.filter (a = ·)) := by rw [count, countP_eq_card_filter]

Count Equals Filtered Cardinality for Multiset Elements

Informal description

For any multiset $s$ over a type $\alpha$ with decidable equality and any element $a \in \alpha$, the count of $a$ in $s$ equals the cardinality of the filtered multiset consisting of elements equal to $a$. That is, $\text{count}(a, s) = \text{card}(\text{filter } (x \mapsto x = a) \ s)$.

Multiset.map_count_True_eq_filter_card theorem

(s : Multiset α) (p : α → Prop) [DecidablePred p] : (s.map p).count True = card (s.filter p)

Full source

/--
Mapping a multiset through a predicate and counting the `True`s yields the cardinality of the set
filtered by the predicate. Note that this uses the notion of a multiset of `Prop`s - 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](https://github.com/leanprover-community/mathlib/pull/11306#discussion_r782286812)
for more discussion.
-/
@[simp]
theorem map_count_True_eq_filter_card (s : Multiset α) (p : α → Prop) [DecidablePred p] :
    (s.map p).count True = card (s.filter p) := by
  simp only [count_eq_card_filter_eq, filter_map, card_map, Function.id_comp,
    eq_true_eq_id, Function.comp_apply]

Count of True in Mapped Predicate Equals Filtered Cardinality

Informal description

For any multiset $s$ over a type $\alpha$ and any decidable predicate $p$ on $\alpha$, the count of `True` in the multiset obtained by mapping $p$ over $s$ equals the cardinality of the multiset filtered by $p$. That is, \[ \text{count}(\text{True}, \text{map } p \ s) = \text{card}(\text{filter } p \ s). \]

Multiset.filter_attach' theorem

 (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] :
  s.attach.filter p = (s.filter fun x ↦ ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ ↦ mem_of_mem_filter)

Full source

lemma filter_attach' (s : Multiset α) (p : {a // a ∈ s} → Prop) [DecidableEq α]
    [DecidablePred p] :
    s.attach.filter p =
      (s.filter fun x ↦ ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ ↦ mem_of_mem_filter) := by
  classical
  refine Multiset.map_injective Subtype.val_injective ?_
  rw [map_filter' _ Subtype.val_injective]
  simp only [Function.comp, Subtype.exists, coe_mk, Subtype.map,
    exists_and_right, exists_eq_right, attach_map_val, map_map, map_coe, id]

Filter-Attach Commutation for Multisets

Informal description

Let $s$ be a multiset over a type $\alpha$ with decidable equality, and let $p$ be a decidable predicate on the subtype $\{a \mid a \in s\}$. Then the filtered multiset of the attached multiset $s.\text{attach}$ under $p$ is equal to the attached multiset of the filtered multiset $\text{filter}\, (\lambda x, \exists h, p \langle x, h \rangle)\, s$, mapped by the identity function on the first component and the proof that filtered elements are in $s$ on the second component. In symbols: \[ \text{filter}\, p\, (s.\text{attach}) = \left(\text{filter}\, (\lambda x, \exists h, p \langle x, h \rangle)\, s\right).\text{attach}.\text{map}\, \left(\text{Subtype.map}\, \text{id}\, (\lambda \_, \text{mem\_of\_mem\_filter})\right). \]

Multiset.Nodup.filter theorem

(p : α → Prop) [DecidablePred p] {s} : Nodup s → Nodup (filter p s)

Full source

theorem Nodup.filter (p : α → Prop) [DecidablePred p] {s} : Nodup s → Nodup (filter p s) :=
  Quot.induction_on s fun _ => List.Nodup.filter (p ·)

Preservation of Nodup under Multiset Filtering

Informal description

For any decidable predicate $p$ on elements of type $\alpha$ and any multiset $s$ of elements in $\alpha$, if $s$ has no duplicate elements (i.e., is nodup), then the filtered multiset $\text{filter } p \ s$ also has no duplicate elements.

Multiset.Nodup.erase_eq_filter theorem

[DecidableEq α] (a : α) {s} : Nodup s → s.erase a = Multiset.filter (· ≠ a) s

Full source

theorem Nodup.erase_eq_filter [DecidableEq α] (a : α) {s} :
    Nodup s → s.erase a = Multiset.filter (· ≠ a) s :=
  Quot.induction_on s fun _ d =>
    congr_arg ((↑) : List α → Multiset α) <| by simpa using List.Nodup.erase_eq_filter d a

Erase equals filter for distinct multisets: $s \setminus \{a\} = \text{filter}(\neq a, s)$

Informal description

For any distinct-element multiset $s$ over a type $\alpha$ with decidable equality, and for any element $a \in \alpha$, the multiset obtained by removing one occurrence of $a$ from $s$ is equal to the multiset obtained by filtering $s$ to keep only elements not equal to $a$.

Multiset.Nodup.filterMap theorem

(f : α → Option β) (H : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') : Nodup s → Nodup (filterMap f s)

Full source

protected theorem Nodup.filterMap (f : α → Option β) (H : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
    Nodup s → Nodup (filterMap f s) :=
  Quot.induction_on s fun _ => List.Nodup.filterMap H

Preservation of Distinctness under Filter and Map Operation on Multisets

Informal description

Let $f : \alpha \to \text{Option } \beta$ be a function and $s$ be a multiset of elements of type $\alpha$. If $f$ satisfies the property that for any $a, a' \in \alpha$ and $b \in \beta$, whenever $b$ is in both $f(a)$ and $f(a')$ then $a = a'$, and if $s$ has no duplicate elements (is `Nodup`), then the filtered and mapped multiset $\text{filterMap } f \ s$ also has no duplicate elements.

Multiset.Nodup.mem_erase_iff theorem

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

Full source

theorem Nodup.mem_erase_iff [DecidableEq α] {a b : α} {l} (d : Nodup l) :
    a ∈ l.erase ba ∈ l.erase b ↔ a ≠ b ∧ a ∈ l := by
  rw [d.erase_eq_filter b, mem_filter, and_comm]

Membership in Erased Multiset for Distinct Elements: $a \in l \setminus \{b\} \leftrightarrow a \neq b \land a \in l$

Informal description

For any distinct-element multiset $l$ over a type $\alpha$ with decidable equality, and for any elements $a, b \in \alpha$, the element $a$ belongs to the multiset obtained by removing one occurrence of $b$ from $l$ if and only if $a \neq b$ and $a$ belongs to $l$.

Multiset.Nodup.not_mem_erase theorem

[DecidableEq α] {a : α} {s} (h : Nodup s) : a ∉ s.erase a

Full source

theorem Nodup.not_mem_erase [DecidableEq α] {a : α} {s} (h : Nodup s) : a ∉ s.erase a := fun ha =>
  (h.mem_erase_iff.1 ha).1 rfl

Non-membership in Self-Erased Distinct Multiset: $a \notin s \setminus \{a\}$

Informal description

For any distinct-element multiset $s$ over a type $\alpha$ with decidable equality, and for any element $a \in \alpha$, the element $a$ does not belong to the multiset obtained by removing one occurrence of $a$ from $s$.

Main definitions