Mathlib.Data.Multiset.MapFold

Multiset.map definition

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

Full source

/-- `map f s` is the lift of the list `map` operation. The multiplicity
  of `b` in `map f s` is the number of `a ∈ s` (counting multiplicity)
  such that `f a = b`. -/
def map (f : α → β) (s : Multiset α) : Multiset β :=
  Quot.liftOn s (fun l : List α => (l.map f : Multiset β)) fun _l₁ _l₂ p => Quot.sound (p.map f)

Image of a multiset under a function

Informal description

Given a function $ f : \alpha \to \beta $ and a multiset $ s $ over $ \alpha $, the multiset $ \text{map } f \ s $ is obtained by applying $ f $ to each element of $ s $. The multiplicity of an element $ b \in \text{map } f \ s $ is the sum of multiplicities of all $ a \in s $ such that $ f(a) = b $.

Multiset.map_congr theorem

{f g : α → β} {s t : Multiset α} : s = t → (∀ x ∈ t, f x = g x) → map f s = map g t

Full source

@[congr]
theorem map_congr {f g : α → β} {s t : Multiset α} :
    s = t → (∀ x ∈ t, f x = g x) → map f s = map g t := by
  rintro rfl h
  induction s using Quot.inductionOn
  exact congr_arg _ (List.map_congr_left h)

Congruence of Multiset Mapping: $\text{map } f \ s = \text{map } g \ t$ when $s = t$ and $f = g$ on $t$

Informal description

Let $f, g : \alpha \to \beta$ be functions and $s, t$ be multisets over $\alpha$. If $s = t$ and for every element $x \in t$ we have $f(x) = g(x)$, then the image multisets satisfy $\text{map } f \ s = \text{map } g \ t$.

Multiset.map_hcongr theorem

 {β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ a ∈ m, HEq (f a) (f' a)) :
  HEq (map f m) (map f' m)

Full source

theorem map_hcongr {β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β')
    (hf : ∀ a ∈ m, HEq (f a) (f' a)) : HEq (map f m) (map f' m) := by
  subst h; simp at hf
  simp [map_congr rfl hf]

Heterogeneous Congruence for Multiset Mapping: $\text{map } f \ m \approx \text{map } f' \ m$ under Type Equality and Pointwise Heterogeneous Equality

Informal description

Let $\alpha$ be a type, and let $\beta$ and $\beta'$ be types with $\beta = \beta'$ (via equality $h$). Given a multiset $m$ over $\alpha$ and functions $f : \alpha \to \beta$ and $f' : \alpha \to \beta'$, if for every element $a \in m$ the values $f(a)$ and $f'(a)$ are heterogeneously equal (i.e., they are equal up to the type equality $\beta = \beta'$), then the mapped multisets $\text{map } f \ m$ and $\text{map } f' \ m$ are also heterogeneously equal.

Multiset.forall_mem_map_iff theorem

{f : α → β} {p : β → Prop} {s : Multiset α} : (∀ y ∈ s.map f, p y) ↔ ∀ x ∈ s, p (f x)

Full source

theorem forall_mem_map_iff {f : α → β} {p : β → Prop} {s : Multiset α} :
    (∀ y ∈ s.map f, p y) ↔ ∀ x ∈ s, p (f x) :=
  Quotient.inductionOn' s fun _L => List.forall_mem_map

Universal Quantification over Mapped Multiset Elements

Informal description

For any function $f : \alpha \to \beta$, predicate $p : \beta \to \mathrm{Prop}$, and multiset $s$ over $\alpha$, the following are equivalent: 1. For every element $y$ in the image multiset $\mathrm{map}\, f\, s$, the predicate $p(y)$ holds. 2. For every element $x$ in the original multiset $s$, the predicate $p(f(x))$ holds.

Multiset.map_coe theorem

(f : α → β) (l : List α) : map f l = l.map f

Full source

@[simp, norm_cast] lemma map_coe (f : α → β) (l : List α) : map f l = l.map f := rfl

Commutativity of Multiset Mapping with List Conversion

Informal description

For any function $f : \alpha \to \beta$ and any list $l$ of elements of type $\alpha$, the multiset obtained by applying $f$ to each element of $l$ (via `Multiset.map`) is equal to the multiset obtained by first converting $l$ to a multiset and then applying $f$ to each element (via `List.map` followed by `Multiset.ofList`). In other words, $\text{map}_\text{Multiset}\, f\, l = \text{ofList}\, (\text{map}_\text{List}\, f\, l)$.

Multiset.map_zero theorem

(f : α → β) : map f 0 = 0

Full source

@[simp]
theorem map_zero (f : α → β) : map f 0 = 0 :=
  rfl

Empty Multiset Maps to Empty Multiset

Informal description

For any function $f : \alpha \to \beta$, the image of the empty multiset under $f$ is the empty multiset, i.e., $\text{map}\, f\, 0 = 0$.

Multiset.map_cons theorem

(f : α → β) (a s) : map f (a ::ₘ s) = f a ::ₘ map f s

Full source

@[simp]
theorem map_cons (f : α → β) (a s) : map f (a ::ₘ s) = f a ::ₘ map f s :=
  Quot.inductionOn s fun _l => rfl

Mapping Function over Multiset Cons

Informal description

For any function $f : \alpha \to \beta$, any element $a \in \alpha$, and any multiset $s$ over $\alpha$, the image of the multiset $a ::ₘ s$ under $f$ is equal to $f(a) ::ₘ \text{map}\, f\, s$.

Multiset.map_comp_cons theorem

(f : α → β) (t) : map f ∘ cons t = cons (f t) ∘ map f

Full source

theorem map_comp_cons (f : α → β) (t) : mapmap f ∘ cons t = conscons (f t) ∘ map f := by
  ext
  simp

Commutativity of Mapping and Insertion Operations on Multisets

Informal description

For any function $f \colon \alpha \to \beta$ and any element $t \in \alpha$, the composition of the mapping operation $\text{map}\, f$ with the insertion operation $\text{cons}\, t$ is equal to the composition of the insertion operation $\text{cons}\, (f t)$ with $\text{map}\, f$. In other words, the following diagram commutes: \[ \text{map}\, f \circ \text{cons}\, t = \text{cons}\, (f t) \circ \text{map}\, f. \]

Multiset.map_singleton theorem

(f : α → β) (a : α) : ({ a } : Multiset α).map f = {f a}

Full source

@[simp]
theorem map_singleton (f : α → β) (a : α) : ({a} : Multiset α).map f = {f a} :=
  rfl

Image of Singleton Multiset under a Function is Singleton of Image

Informal description

For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the image of the singleton multiset $\{a\}$ under $f$ is the singleton multiset $\{f(a)\}$.

Multiset.map_replicate theorem

(f : α → β) (k : ℕ) (a : α) : (replicate k a).map f = replicate k (f a)

Full source

@[simp]
theorem map_replicate (f : α → β) (k : ℕ) (a : α) : (replicate k a).map f = replicate k (f a) := by
  simp only [← coe_replicate, map_coe, List.map_replicate]

Image of Replicated Multiset under a Function is Replicated Image

Informal description

For any function $f \colon \alpha \to \beta$, any natural number $k$, and any element $a \in \alpha$, the image under $f$ of the multiset consisting of $k$ copies of $a$ is equal to the multiset consisting of $k$ copies of $f(a)$. That is, \[ \text{map } f (\text{replicate } k \ a) = \text{replicate } k \ (f a). \]

Multiset.map_add theorem

(f : α → β) (s t) : map f (s + t) = map f s + map f t

Full source

@[simp]
theorem map_add (f : α → β) (s t) : map f (s + t) = map f s + map f t :=
  Quotient.inductionOn₂ s t fun _l₁ _l₂ => congr_arg _ map_append

Additivity of Multiset Mapping: $\text{map } f (s + t) = \text{map } f s + \text{map } f t$

Informal description

For any function $f \colon \alpha \to \beta$ and any multisets $s, t$ over $\alpha$, the image of the sum $s + t$ under $f$ is equal to the sum of the images of $s$ and $t$ under $f$, i.e., \[ \text{map } f (s + t) = \text{map } f s + \text{map } f t. \]

Multiset.canLift instance

(c) (p) [CanLift α β c p] : CanLift (Multiset α) (Multiset β) (map c) fun s => ∀ x ∈ s, p x

Full source

/-- If each element of `s : Multiset α` can be lifted to `β`, then `s` can be lifted to
`Multiset β`. -/
instance canLift (c) (p) [CanLift α β c p] :
    CanLift (Multiset α) (Multiset β) (map c) fun s => ∀ x ∈ s, p x where
  prf := by
    rintro ⟨l⟩ hl
    lift l to List β using hl
    exact ⟨l, map_coe _ _⟩

Lifting Condition for Multisets

Informal description

For any types $\alpha$ and $\beta$ with a lifting condition specified by `CanLift α β c p`, where $c : \beta \to \alpha$ is the lifting function and $p : \alpha \to \text{Prop}$ is the condition, the multiset type `Multiset α` can be lifted to `Multiset β` via the function `Multiset.map c`, provided that every element $x$ in the multiset satisfies $p(x)$. In other words, if every element of a multiset can be lifted from $\alpha$ to $\beta$ under condition $p$, then the entire multiset can be lifted to a multiset over $\beta$ using the mapping function $c$.

Multiset.mem_map theorem

{f : α → β} {b : β} {s : Multiset α} : b ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b

Full source

@[simp]
theorem mem_map {f : α → β} {b : β} {s : Multiset α} : b ∈ map f sb ∈ map f s ↔ ∃ a, a ∈ s ∧ f a = b :=
  Quot.inductionOn s fun _l => List.mem_map

Characterization of Membership in Mapped Multiset: $b \in \text{map } f \ s \leftrightarrow \exists a \in s, f(a) = b$

Informal description

For any function $f \colon \alpha \to \beta$, element $b \in \beta$, and multiset $s$ over $\alpha$, the element $b$ belongs to the image multiset $\text{map } f \ s$ if and only if there exists an element $a \in s$ such that $f(a) = b$.

Multiset.card_map theorem

(f : α → β) (s) : card (map f s) = card s

Full source

@[simp]
theorem card_map (f : α → β) (s) : card (map f s) = card s :=
  Quot.inductionOn s fun _ => length_map _

Cardinality Preservation under Multiset Mapping

Informal description

For any function $f \colon \alpha \to \beta$ and multiset $s$ over $\alpha$, the cardinality of the image multiset $\text{map } f \ s$ is equal to the cardinality of $s$. That is, $|\text{map } f \ s| = |s|$.

Multiset.map_eq_zero theorem

{s : Multiset α} {f : α → β} : s.map f = 0 ↔ s = 0

Full source

@[simp]
theorem map_eq_zero {s : Multiset α} {f : α → β} : s.map f = 0 ↔ s = 0 := by
  rw [← Multiset.card_eq_zero, Multiset.card_map, Multiset.card_eq_zero]

Empty Multiset Characterization under Mapping: $\text{map } f \ s = 0 \leftrightarrow s = 0$

Informal description

For any multiset $s$ over a type $\alpha$ and any function $f \colon \alpha \to \beta$, the image of $s$ under $f$ is the empty multiset if and only if $s$ itself is the empty multiset. That is, $\text{map } f \ s = 0 \leftrightarrow s = 0$.

Multiset.mem_map_of_mem theorem

(f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) : f a ∈ map f s

Full source

theorem mem_map_of_mem (f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) : f a ∈ map f s :=
  mem_map.2 ⟨_, h, rfl⟩

Image of Element in Mapped Multiset: $a \in s \to f(a) \in \text{map } f \ s$

Informal description

For any function $f \colon \alpha \to \beta$, element $a \in \alpha$, and multiset $s$ over $\alpha$, if $a$ belongs to $s$, then $f(a)$ belongs to the image multiset $\text{map } f \ s$.

Multiset.map_eq_singleton theorem

{f : α → β} {s : Multiset α} {b : β} : map f s = { b } ↔ ∃ a : α, s = { a } ∧ f a = b

Full source

theorem map_eq_singleton {f : α → β} {s : Multiset α} {b : β} :
    mapmap f s = {b} ↔ ∃ a : α, s = {a} ∧ f a = b := by
  constructor
  · intro h
    obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]
  · rintro ⟨a, rfl, rfl⟩
    simp

Characterization of Singleton Image Multisets: $\mathrm{map}\,f\,s = \{b\} \leftrightarrow \exists a, s = \{a\} \wedge f(a) = b$

Informal description

For any function $f \colon \alpha \to \beta$, multiset $s$ over $\alpha$, and element $b \in \beta$, the image of $s$ under $f$ is the singleton multiset $\{b\}$ if and only if there exists an element $a \in \alpha$ such that $s$ is the singleton multiset $\{a\}$ and $f(a) = b$.

Multiset.map_eq_cons theorem

 [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :
  (∃ a ∈ s, f a = b ∧ (s.erase a).map f = t) ↔ s.map f = b ::ₘ t

Full source

theorem map_eq_cons [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :
    (∃ a ∈ s, f a = b ∧ (s.erase a).map f = t) ↔ s.map f = b ::ₘ t := by
  constructor
  · rintro ⟨a, ha, rfl, rfl⟩
    rw [← map_cons, Multiset.cons_erase ha]
  · intro h
    have : b ∈ s.map f := by
      rw [h]
      exact mem_cons_self _ _
    obtain ⟨a, h1, rfl⟩ := mem_map.mp this
    obtain ⟨u, rfl⟩ := exists_cons_of_mem h1
    rw [map_cons, cons_inj_right] at h
    refine ⟨a, mem_cons_self _ _, rfl, ?_⟩
    rw [Multiset.erase_cons_head, h]

Characterization of Multiset Image as Cons: $\text{map } f s = b ::ₘ t \leftrightarrow \exists a \in s, f(a) = b \land \text{map } f (s \setminus \{a\}) = t$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\alpha$. For any function $f : \alpha \to \beta$, multisets $s$ over $\alpha$ and $t$ over $\beta$, and element $b \in \beta$, the following are equivalent: 1. There exists an element $a \in s$ such that $f(a) = b$ and the image of $s$ with one occurrence of $a$ removed under $f$ equals $t$. 2. The image of $s$ under $f$ equals the multiset obtained by inserting $b$ into $t$. In symbols: \[ \big(\exists a \in s, f(a) = b \land \text{map } f (s \setminus \{a\}) = t\big) \leftrightarrow \text{map } f s = b ::ₘ t \]

Multiset.mem_map_of_injective theorem

{f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} : f a ∈ map f s ↔ a ∈ s

Full source

@[simp 1100, nolint simpNF]
theorem mem_map_of_injective {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} :
    f a ∈ map f sf a ∈ map f s ↔ a ∈ s :=
  Quot.inductionOn s fun _l => List.mem_map_of_injective H

Membership Preservation under Injective Mapping for Multisets

Informal description

For any injective function $f : \alpha \to \beta$, element $a \in \alpha$, and multiset $s$ over $\alpha$, the image $f(a)$ belongs to the multiset $\mathrm{map}\,f\,s$ if and only if $a$ belongs to $s$.

Multiset.map_map theorem

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

Full source

@[simp]
theorem map_map (g : β → γ) (f : α → β) (s : Multiset α) : map g (map f s) = map (g ∘ f) s :=
  Quot.inductionOn s fun _l => congr_arg _ List.map_map

Composition of Multiset Maps: $\mathrm{map}\,g \circ \mathrm{map}\,f = \mathrm{map}\,(g \circ f)$

Informal description

For any functions $g : \beta \to \gamma$ and $f : \alpha \to \beta$, and any multiset $s$ over $\alpha$, the image of $s$ under the composition $g \circ f$ is equal to the image under $g$ of the image of $s$ under $f$, i.e., \[ \mathrm{map}\,g\,(\mathrm{map}\,f\,s) = \mathrm{map}\,(g \circ f)\,s. \]

Multiset.map_id theorem

(s : Multiset α) : map id s = s

Full source

theorem map_id (s : Multiset α) : map id s = s :=
  Quot.inductionOn s fun _l => congr_arg _ <| List.map_id _

Identity Mapping Preserves Multiset

Informal description

For any multiset $s$ over a type $\alpha$, the image of $s$ under the identity function $\mathrm{id}$ is equal to $s$ itself, i.e., $\mathrm{map}\ \mathrm{id}\ s = s$.

Multiset.map_id' theorem

(s : Multiset α) : map (fun x => x) s = s

Full source

@[simp]
theorem map_id' (s : Multiset α) : map (fun x => x) s = s :=
  map_id s

Identity Mapping Preserves Multiset (alternative form)

Informal description

For any multiset $s$ over a type $\alpha$, the image of $s$ under the identity function $\lambda x, x$ is equal to $s$ itself, i.e., $\mathrm{map}\,(\lambda x, x)\,s = s$.

Multiset.map_const theorem

(s : Multiset α) (b : β) : map (const α b) s = replicate (card s) b

Full source

theorem map_const (s : Multiset α) (b : β) : map (const α b) s = replicate (card s) b :=
  Quot.inductionOn s fun _ => congr_arg _ List.map_const'

Image of Multiset under Constant Function is Replicated Element

Informal description

For any multiset $s$ over a type $\alpha$ and any element $b$ of type $\beta$, the image of $s$ under the constant function $f(x) = b$ is equal to the multiset consisting of $b$ repeated $\text{card}(s)$ times, i.e., $\text{map} (\lambda x, b) s = \text{replicate} (\text{card} s) b$.

Multiset.map_const' theorem

(s : Multiset α) (b : β) : map (fun _ ↦ b) s = replicate (card s) b

Full source

@[simp] theorem map_const' (s : Multiset α) (b : β) : map (fun _ ↦ b) s = replicate (card s) b :=
  map_const _ _

Image of Multiset under Constant Function Equals Replicated Element

Informal description

For any multiset $s$ over a type $\alpha$ and any element $b$ of type $\beta$, the image of $s$ under the constant function that maps every element to $b$ is equal to the multiset consisting of $b$ repeated $\text{card}(s)$ times, i.e., $\text{map} (\lambda \_, b) s = \text{replicate} (\text{card} s) b$.

Multiset.map_le_map theorem

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

Full source

@[simp, gcongr]
theorem map_le_map {f : α → β} {s t : Multiset α} (h : s ≤ t) : map f s ≤ map f t :=
  leInductionOn h fun h => (h.map f).subperm

Monotonicity of Multiset Mapping: $s \leq t \implies \text{map } f \ s \leq \text{map } f \ t$

Informal description

For any function $f : \alpha \to \beta$ and multisets $s, t$ over $\alpha$, if $s \leq t$ in the sub-multiset order, then the image of $s$ under $f$ is a sub-multiset of the image of $t$ under $f$, i.e., $\text{map } f \ s \leq \text{map } f \ t$.

Multiset.map_lt_map theorem

{f : α → β} {s t : Multiset α} (h : s < t) : s.map f < t.map f

Full source

@[simp, gcongr]
theorem map_lt_map {f : α → β} {s t : Multiset α} (h : s < t) : s.map f < t.map f := by
  refine (map_le_map h.le).lt_of_not_le fun H => h.ne <| eq_of_le_of_card_le h.le ?_
  rw [← s.card_map f, ← t.card_map f]
  exact card_le_card H

Strict Monotonicity of Multiset Mapping: $s < t \implies \text{map } f \ s < \text{map } f \ t$

Informal description

For any function $f \colon \alpha \to \beta$ and multisets $s, t$ over $\alpha$, if $s$ is strictly contained in $t$ (i.e., $s < t$), then the image of $s$ under $f$ is strictly contained in the image of $t$ under $f$, i.e., $\text{map } f \ s < \text{map } f \ t$.

Multiset.map_mono theorem

(f : α → β) : Monotone (map f)

Full source

theorem map_mono (f : α → β) : Monotone (map f) := fun _ _ => map_le_map

Monotonicity of Multiset Mapping: $\text{map } f$ Preserves Sub-Multiset Order

Informal description

For any function $f \colon \alpha \to \beta$, the mapping operation $\text{map } f$ on multisets is monotone with respect to the sub-multiset order. That is, for any multisets $s, t$ over $\alpha$, if $s \leq t$, then $\text{map } f \ s \leq \text{map } f \ t$.

Multiset.map_strictMono theorem

(f : α → β) : StrictMono (map f)

Full source

theorem map_strictMono (f : α → β) : StrictMono (map f) := fun _ _ => map_lt_map

Strict Monotonicity of Multiset Mapping: $s < t \implies \text{map } f \ s < \text{map } f \ t$

Informal description

For any function $f \colon \alpha \to \beta$, the mapping operation $\text{map } f$ on multisets is strictly monotone with respect to the strict sub-multiset order. That is, for any multisets $s, t$ over $\alpha$, if $s < t$, then $\text{map } f \ s < \text{map } f \ t$.

Multiset.map_subset_map theorem

{f : α → β} {s t : Multiset α} (H : s ⊆ t) : map f s ⊆ map f t

Full source

@[simp, gcongr]
theorem map_subset_map {f : α → β} {s t : Multiset α} (H : s ⊆ t) : mapmap f s ⊆ map f t := fun _b m =>
  let ⟨a, h, e⟩ := mem_map.1 m
  mem_map.2 ⟨a, H h, e⟩

Image of Subset under Function Preserves Subset Relation: $\text{map } f \ s \subseteq \text{map } f \ t$ when $s \subseteq t$

Informal description

For any function $f \colon \alpha \to \beta$ and multisets $s, t$ over $\alpha$, if $s$ is a subset of $t$, then the image of $s$ under $f$ is a subset of the image of $t$ under $f$, i.e., $\text{map } f \ s \subseteq \text{map } f \ t$.

Multiset.map_erase theorem

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

Full source

theorem map_erase [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α)
    (s : Multiset α) : (s.erase x).map f = (s.map f).erase (f x) := by
  induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
  by_cases hxy : y = x
  · cases hxy
    simp
  · rw [s.erase_cons_tail hxy, map_cons, map_cons, (s.map f).erase_cons_tail (hf.ne hxy), ih]

Image of Multiset Erasure under Injective Function: $\text{map}\, f\, (s \setminus \{x\}) = (\text{map}\, f\, s) \setminus \{f(x)\}$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $f : \alpha \to \beta$ be an injective function. For any element $x \in \alpha$ and any multiset $s$ over $\alpha$, the image of the multiset $s \setminus \{x\}$ under $f$ is equal to the multiset $\text{map}\, f\, s$ with one occurrence of $f(x)$ removed. That is, $$ \text{map}\, f\, (s \setminus \{x\}) = (\text{map}\, f\, s) \setminus \{f(x)\}. $$

Multiset.map_erase_of_mem theorem

 [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) {x : α} (h : x ∈ s) :
  (s.erase x).map f = (s.map f).erase (f x)

Full source

theorem map_erase_of_mem [DecidableEq α] [DecidableEq β] (f : α → β)
    (s : Multiset α) {x : α} (h : x ∈ s) : (s.erase x).map f = (s.map f).erase (f x) := by
  induction s using Multiset.induction_on with | empty => simp | cons y s ih => ?_
  rcases eq_or_ne y x with rfl | hxy
  · simp
  replace h : x ∈ s := by simpa [hxy.symm] using h
  rw [s.erase_cons_tail hxy, map_cons, map_cons, ih h, erase_cons_tail_of_mem (mem_map_of_mem f h)]

Image of Multiset Erasure under Function: $\text{map}\, f\, (s \setminus \{x\}) = (\text{map}\, f\, s) \setminus \{f(x)\}$ for $x \in s$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality, and let $f : \alpha \to \beta$ be a function. For any multiset $s$ over $\alpha$ and any element $x \in s$, the image of the multiset $s \setminus \{x\}$ under $f$ is equal to the multiset $\text{map}\, f\, s$ with one occurrence of $f(x)$ removed. That is, $$ \text{map}\, f\, (s \setminus \{x\}) = (\text{map}\, f\, s) \setminus \{f(x)\}. $$

Multiset.map_surjective_of_surjective theorem

{f : α → β} (hf : Function.Surjective f) : Function.Surjective (map f)

Full source

theorem map_surjective_of_surjective {f : α → β} (hf : Function.Surjective f) :
    Function.Surjective (map f) := by
  intro s
  induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

Surjectivity of Multiset Mapping Induced by a Surjective Function

Informal description

For any surjective function $f : \alpha \to \beta$, the induced map $\text{map}\, f : \text{Multiset}\, \alpha \to \text{Multiset}\, \beta$ is also surjective. That is, for every multiset $t$ over $\beta$, there exists a multiset $s$ over $\alpha$ such that $\text{map}\, f\, s = t$.

Multiset.foldl definition

(f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) : β

Full source

/-- `foldl f H b s` is the lift of the list operation `foldl f b l`,
  which folds `f` over the multiset. It is well defined when `f` is right-commutative,
  that is, `f (f b a₁) a₂ = f (f b a₂) a₁`. -/
def foldl (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) : β :=
  Quot.liftOn s (fun l => List.foldl f b l) fun _l₁ _l₂ p => p.foldl_eq b

Left fold over a multiset with a right-commutative operation

Informal description

Given a right-commutative operation $f : \beta \to \alpha \to \beta$, an initial value $b \in \beta$, and a multiset $s$ over $\alpha$, the left fold $\text{foldl}~f~b~s$ is defined as the result of folding $f$ over the elements of $s$ starting with $b$, where the order of folding does not matter due to the right-commutativity of $f$. More precisely, for any list $l$ representing the multiset $s$, $\text{foldl}~f~b~s$ is equal to $\text{foldl}~f~b~l$, and this definition is independent of the choice of $l$ up to permutation of its elements.

Multiset.foldl_zero theorem

(b) : foldl f b 0 = b

Full source

@[simp]
theorem foldl_zero (b) : foldl f b 0 = b :=
  rfl

Left Fold over Empty Multiset Yields Initial Value

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$ and initial value $b \in \beta$, the left fold over the empty multiset satisfies $\text{foldl}_f\,b\,0 = b$.

Multiset.foldl_cons theorem

(b a s) : foldl f b (a ::ₘ s) = foldl f (f b a) s

Full source

@[simp]
theorem foldl_cons (b a s) : foldl f b (a ::ₘ s) = foldl f (f b a) s :=
  Quot.inductionOn s fun _l => rfl

Left Fold Recursion for Multiset Insertion: $\text{foldl}_f\,b\,(a \cup s) = \text{foldl}_f\,(f(b, a))\,s$

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$, initial value $b \in \beta$, element $a \in \alpha$, and multiset $s$ over $\alpha$, the left fold satisfies: \[ \text{foldl}_f\,b\,(a \cup s) = \text{foldl}_f\,(f(b, a))\,s \] where $a \cup s$ denotes the multiset obtained by adding one occurrence of $a$ to $s$.

Multiset.foldl_add theorem

(b s t) : foldl f b (s + t) = foldl f (foldl f b s) t

Full source

@[simp]
theorem foldl_add (b s t) : foldl f b (s + t) = foldl f (foldl f b s) t :=
  Quotient.inductionOn₂ s t fun _ _ => foldl_append

Additivity of Left Fold over Multiset Union

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$, initial value $b \in \beta$, and multisets $s, t$ over $\alpha$, the left fold satisfies the additive property: \[ \text{foldl}_f\,b\,(s + t) = \text{foldl}_f\,(\text{foldl}_f\,b\,s)\,t \]

Multiset.foldr definition

(f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) : β

Full source

/-- `foldr f H b s` is the lift of the list operation `foldr f b l`,
  which folds `f` over the multiset. It is well defined when `f` is left-commutative,
  that is, `f a₁ (f a₂ b) = f a₂ (f a₁ b)`. -/
def foldr (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) : β :=
  Quot.liftOn s (fun l => List.foldr f b l) fun _l₁ _l₂ p => p.foldr_eq b

Right fold over a multiset with a left-commutative operation

Informal description

Given a left-commutative operation $f : \alpha \to \beta \to \beta$, an initial value $b \in \beta$, and a multiset $s$ of elements of type $\alpha$, the function `foldr` computes the right fold of $f$ over $s$ starting with $b$. This is well-defined because the result is invariant under permutations of the elements in $s$ due to the left-commutativity of $f$.

Multiset.foldr_zero theorem

(b) : foldr f b 0 = b

Full source

@[simp]
theorem foldr_zero (b) : foldr f b 0 = b :=
  rfl

Right Fold of Empty Multiset Yields Initial Value

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$ and any initial value $b \in \beta$, the right fold of $f$ over the empty multiset $0$ is equal to $b$, i.e., $\text{foldr}_f(b, 0) = b$.

Multiset.foldr_cons theorem

(b a s) : foldr f b (a ::ₘ s) = f a (foldr f b s)

Full source

@[simp]
theorem foldr_cons (b a s) : foldr f b (a ::ₘ s) = f a (foldr f b s) :=
  Quot.inductionOn s fun _l => rfl

Right Fold Recursion for Multiset Insertion

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, element $a \in \alpha$, and multiset $s$ over $\alpha$, the right fold of $f$ over the multiset obtained by inserting $a$ into $s$ satisfies: $$ \text{foldr}_f\, b\, (a \text{ ::ₘ } s) = f\, a\, (\text{foldr}_f\, b\, s). $$

Multiset.foldr_singleton theorem

(b a) : foldr f b ({ a } : Multiset α) = f a b

Full source

@[simp]
theorem foldr_singleton (b a) : foldr f b ({a} : Multiset α) = f a b :=
  rfl

Right Fold over Singleton Multiset with Left-Commutative Operation

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, and element $a \in \alpha$, the right fold of $f$ over the singleton multiset $\{a\}$ starting with $b$ equals $f(a, b)$. In symbols: $$\text{foldr}_f\, b\, \{a\} = f\, a\, b.$$

Multiset.foldr_add theorem

(b s t) : foldr f b (s + t) = foldr f (foldr f b t) s

Full source

@[simp]
theorem foldr_add (b s t) : foldr f b (s + t) = foldr f (foldr f b t) s :=
  Quotient.inductionOn₂ s t fun _ _ => foldr_append

Right Fold over Multiset Sum with Left-Commutative Operation

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, and multisets $s, t$ over $\alpha$, the right fold of $f$ over the sum $s + t$ starting with $b$ equals the right fold of $f$ over $s$ starting with the right fold of $f$ over $t$ starting with $b$. In symbols: $$\text{foldr}_f\, b\, (s + t) = \text{foldr}_f\, (\text{foldr}_f\, b\, t)\, s.$$

Multiset.coe_foldr theorem

(f : α → β → β) [LeftCommutative f] (b : β) (l : List α) : foldr f b l = l.foldr f b

Full source

@[simp]
theorem coe_foldr (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) :
    foldr f b l = l.foldr f b :=
  rfl

Equality of Right Folds for Multiset and List Construction

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, and list $l$ of elements of type $\alpha$, the right fold of $f$ over the multiset constructed from $l$ is equal to the right fold of $f$ over the list $l$ itself. In symbols: \[ \text{foldr}_f\, b\, \{l\} = \text{foldr}_f\, b\, l \] where $\{l\}$ denotes the multiset obtained from the list $l$.

Multiset.coe_foldl theorem

(f : β → α → β) [RightCommutative f] (b : β) (l : List α) : foldl f b l = l.foldl f b

Full source

@[simp]
theorem coe_foldl (f : β → α → β) [RightCommutative f] (b : β) (l : List α) :
    foldl f b l = l.foldl f b :=
  rfl

Equality of Left Folds for Multiset and List Construction

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$, initial value $b \in \beta$, and list $l$ of elements of type $\alpha$, the left fold of $f$ over the multiset constructed from $l$ is equal to the left fold of $f$ over the list $l$ itself. In symbols: \[ \text{foldl}_f\, b\, \{l\} = \text{foldl}_f\, b\, l \] where $\{l\}$ denotes the multiset obtained from the list $l$.

Multiset.coe_foldr_swap theorem

(f : α → β → β) [LeftCommutative f] (b : β) (l : List α) : foldr f b l = l.foldl (fun x y => f y x) b

Full source

theorem coe_foldr_swap (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) :
    foldr f b l = l.foldl (fun x y => f y x) b :=
  (congr_arg (foldr f b) (coe_reverse l)).symm.trans foldr_reverse

Equality between multiset right fold and list left fold with swapped operation

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, and list $l$ of elements of type $\alpha$, the right fold of $f$ over the multiset constructed from $l$ equals the left fold of the swapped operation $\lambda x y, f y x$ over the original list $l$. That is, \[ \text{foldr}_f b \{l\} = \text{foldl}_{(\lambda x y, f y x)} b l \] where $\{l\}$ denotes the multiset obtained from list $l$.

Multiset.foldr_swap theorem

(f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) : foldr f b s = foldl (fun x y => f y x) b s

Full source

theorem foldr_swap (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) :
    foldr f b s = foldl (fun x y => f y x) b s :=
  Quot.inductionOn s fun _l => coe_foldr_swap _ _ _

Equivalence of Right Fold and Swapped Left Fold for Left-Commutative Operations on Multisets

Informal description

For any left-commutative operation $f : \alpha \to \beta \to \beta$, initial value $b \in \beta$, and multiset $s$ over $\alpha$, the right fold of $f$ over $s$ starting with $b$ equals the left fold of the swapped operation $(x, y) \mapsto f y x$ over $s$ starting with $b$. That is, \[ \text{foldr}_f\, b\, s = \text{foldl}_{(x\, y \mapsto f\, y\, x)}\, b\, s. \]

Multiset.foldl_swap theorem

(f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) : foldl f b s = foldr (fun x y => f y x) b s

Full source

theorem foldl_swap (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) :
    foldl f b s = foldr (fun x y => f y x) b s :=
  (foldr_swap _ _ _).symm

Equivalence of Left Fold and Swapped Right Fold for Right-Commutative Operations on Multisets

Informal description

For any right-commutative operation $f : \beta \to \alpha \to \beta$, initial value $b \in \beta$, and multiset $s$ over $\alpha$, the left fold of $f$ over $s$ starting with $b$ equals the right fold of the swapped operation $(x, y) \mapsto f y x$ over $s$ starting with $b$. That is, \[ \text{foldl}_f\, b\, s = \text{foldr}_{(x\, y \mapsto f\, y\, x)}\, b\, s. \]

Multiset.foldr_induction' theorem

 (f : α → β → β) [LeftCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α)
  (hpqf : ∀ a b, q a → p b → p (f a b)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldr f x s)

Full source

theorem foldr_induction' (f : α → β → β) [LeftCommutative f] (x : β) (q : α → Prop)
    (p : β → Prop) (s : Multiset α) (hpqf : ∀ a b, q a → p b → p (f a b)) (px : p x)
    (q_s : ∀ a ∈ s, q a) : p (foldr f x s) := by
  induction s using Multiset.induction with
  | empty => simpa
  | cons a s ihs =>
    simp only [forall_mem_cons, foldr_cons] at q_s ⊢
    exact hpqf _ _ q_s.1 (ihs q_s.2)

Induction Principle for Right Fold over Multisets with Left-Commutative Operation

Informal description

Let $f : \alpha \to \beta \to \beta$ be a left-commutative operation, $x \in \beta$ an initial value, $q : \alpha \to \mathrm{Prop}$ a predicate on $\alpha$, and $p : \beta \to \mathrm{Prop}$ a predicate on $\beta$. For any multiset $s$ over $\alpha$, if: 1. For all $a \in \alpha$ and $b \in \beta$, $q(a)$ and $p(b)$ imply $p(f(a, b))$, 2. $p(x)$ holds, and 3. For all $a \in s$, $q(a)$ holds, then $p(\mathrm{foldr}_f\, x\, s)$ holds.

Multiset.foldr_induction theorem

 (f : α → α → α) [LeftCommutative f] (x : α) (p : α → Prop) (s : Multiset α) (p_f : ∀ a b, p a → p b → p (f a b))
  (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldr f x s)

Full source

theorem foldr_induction (f : α → α → α) [LeftCommutative f] (x : α) (p : α → Prop)
    (s : Multiset α) (p_f : ∀ a b, p a → p b → p (f a b)) (px : p x) (p_s : ∀ a ∈ s, p a) :
    p (foldr f x s) :=
  foldr_induction' f x p p s p_f px p_s

Induction Principle for Right Fold over Multisets with Left-Commutative Operation

Informal description

Let $f : \alpha \to \alpha \to \alpha$ be a left-commutative operation, $x \in \alpha$ an initial value, and $p : \alpha \to \mathrm{Prop}$ a predicate on $\alpha$. For any multiset $s$ over $\alpha$, if: 1. For all $a, b \in \alpha$, $p(a)$ and $p(b)$ imply $p(f(a, b))$, 2. $p(x)$ holds, and 3. For all $a \in s$, $p(a)$ holds, then $p(\mathrm{foldr}_f\, x\, s)$ holds.

Multiset.foldl_induction' theorem

 (f : β → α → β) [RightCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α)
  (hpqf : ∀ a b, q a → p b → p (f b a)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldl f x s)

Full source

theorem foldl_induction' (f : β → α → β) [RightCommutative f] (x : β) (q : α → Prop)
    (p : β → Prop) (s : Multiset α) (hpqf : ∀ a b, q a → p b → p (f b a)) (px : p x)
    (q_s : ∀ a ∈ s, q a) : p (foldl f x s) := by
  rw [foldl_swap]
  exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s

Induction Principle for Left Fold over Multisets with Right-Commutative Operation

Informal description

Let $f : \beta \to \alpha \to \beta$ be a right-commutative operation, $x \in \beta$ an initial value, $q : \alpha \to \mathrm{Prop}$ a predicate on $\alpha$, and $p : \beta \to \mathrm{Prop}$ a predicate on $\beta$. For any multiset $s$ over $\alpha$, if: 1. For all $a \in \alpha$ and $b \in \beta$, $q(a)$ and $p(b)$ imply $p(f(b, a))$, 2. $p(x)$ holds, and 3. For all $a \in s$, $q(a)$ holds, then $p(\mathrm{foldl}_f\, x\, s)$ holds.

Multiset.foldl_induction theorem

 (f : α → α → α) [RightCommutative f] (x : α) (p : α → Prop) (s : Multiset α) (p_f : ∀ a b, p a → p b → p (f b a))
  (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldl f x s)

Full source

theorem foldl_induction (f : α → α → α) [RightCommutative f] (x : α) (p : α → Prop)
    (s : Multiset α) (p_f : ∀ a b, p a → p b → p (f b a)) (px : p x) (p_s : ∀ a ∈ s, p a) :
    p (foldl f x s) :=
  foldl_induction' f x p p s p_f px p_s

Induction Principle for Left Fold over Multisets with Right-Commutative Operation

Informal description

Let $f : \alpha \to \alpha \to \alpha$ be a right-commutative operation, $x \in \alpha$ an initial value, and $p : \alpha \to \mathrm{Prop}$ a predicate on $\alpha$. For any multiset $s$ over $\alpha$, if: 1. For all $a, b \in \alpha$, $p(a)$ and $p(b)$ imply $p(f(b, a))$, 2. $p(x)$ holds, and 3. For all $a \in s$, $p(a)$ holds, then $p(\mathrm{foldl}_f\, x\, s)$ holds.

Multiset.pmap_eq_map theorem

(p : α → Prop) (f : α → β) (s : Multiset α) : ∀ H, @pmap _ _ p (fun a _ => f a) s H = map f s

Full source

theorem pmap_eq_map (p : α → Prop) (f : α → β) (s : Multiset α) :
    ∀ H, @pmap _ _ p (fun a _ => f a) s H = map f s :=
  Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map H

Equality of Partial Map and Standard Map on Multisets

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, function $f : \alpha \to \beta$, and multiset $s$ over $\alpha$, if $H$ is a proof that all elements of $s$ satisfy $p$, then the partial map $\mathrm{pmap}$ (applying $f$ to each element with its proof $H$) is equal to the standard map $\mathrm{map}\ f\ s$.

Multiset.map_pmap theorem

 {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (s) : ∀ H, map g (pmap f s H) = pmap (fun a h => g (f a h)) s H

Full source

theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (s) :
    ∀ H, map g (pmap f s H) = pmap (fun a h => g (f a h)) s H :=
  Quot.inductionOn s fun _ H => congr_arg _ <| List.map_pmap H

Commutativity of Map and Partial Map on Multisets

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a predicate, $g : \beta \to \gamma$ a function, and $f : \forall a, p a \to \beta$ a partial function defined on elements satisfying $p$. For any multiset $s$ over $\alpha$ and any proof $H$ that all elements of $s$ satisfy $p$, we have: \[ \mathrm{map}\ g\ (\mathrm{pmap}\ f\ s\ H) = \mathrm{pmap}\ (\lambda a\ h, g (f a h))\ s\ H \] where $\mathrm{map}$ applies $g$ to each element of a multiset, and $\mathrm{pmap}$ applies $f$ to each element of $s$ along with its proof that it satisfies $p$.

Multiset.pmap_eq_map_attach theorem

{p : α → Prop} (f : ∀ a, p a → β) (s) : ∀ H, pmap f s H = s.attach.map fun x => f x.1 (H _ x.2)

Full source

theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (s) :
    ∀ H, pmap f s H = s.attach.map fun x => f x.1 (H _ x.2) :=
  Quot.inductionOn s fun _ H => congr_arg _ <| List.pmap_eq_map_attach H

Partial Map Equals Map of Attached Multiset

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, partial function $f : \forall a, p a \to \beta$, and multiset $s$ over $\alpha$, if $H$ is a proof that all elements of $s$ satisfy $p$, then the partial map $\mathrm{pmap}\ f\ s\ H$ is equal to the standard map applied to the attached multiset $s.\mathrm{attach}$, where each element $x$ is mapped to $f\ x.1\ (H\ x.1\ x.2)$. Here, $x.1$ denotes the underlying element and $x.2$ its membership proof in $s$.

Multiset.attach_map_val' theorem

(s : Multiset α) (f : α → β) : (s.attach.map fun i => f i.val) = s.map f

Full source

@[simp]
theorem attach_map_val' (s : Multiset α) (f : α → β) : (s.attach.map fun i => f i.val) = s.map f :=
  Quot.inductionOn s fun _ => congr_arg _ List.attach_map_val

Equality of Attached Map and Direct Map for Multisets

Informal description

For any multiset $s$ over a type $\alpha$ and any function $f : \alpha \to \beta$, the multiset obtained by first attaching membership proofs to each element of $s$ and then mapping $f$ over the resulting multiset (applied to the underlying values) is equal to directly mapping $f$ over $s$. In other words, let $s.\text{attach}$ be the multiset $\{(x, h_x) \mid x \in s\}$ where $h_x$ is a proof that $x \in s$. Then: \[ \text{map } (λ (i : \{x \mid x \in s\}), f i.val) \ s.\text{attach} = \text{map } f \ s \]

Multiset.attach_map_val theorem

(s : Multiset α) : s.attach.map Subtype.val = s

Full source

@[simp]
theorem attach_map_val (s : Multiset α) : s.attach.map Subtype.val = s :=
  (attach_map_val' _ _).trans s.map_id

Projection of Attached Multiset Recovers Original Multiset

Informal description

For any multiset $s$ over a type $\alpha$, the image of the attached multiset $s.\mathrm{attach}$ under the projection function $\mathrm{Subtype.val}$ (which extracts the underlying element from each pair) is equal to $s$ itself. In other words, if $s.\mathrm{attach}$ is the multiset $\{(x, h_x) \mid x \in s\}$ where $h_x$ is a proof that $x \in s$, then mapping the first projection over this multiset recovers the original multiset $s$.

Multiset.attach_cons theorem

 (a : α) (m : Multiset α) :
  (a ::ₘ m).attach = ⟨a, mem_cons_self a m⟩ ::ₘ m.attach.map fun p => ⟨p.1, mem_cons_of_mem p.2⟩

Full source

theorem attach_cons (a : α) (m : Multiset α) :
    (a ::ₘ m).attach =
      ⟨a, mem_cons_self a m⟩⟨a, mem_cons_self a m⟩ ::ₘ m.attach.map fun p => ⟨p.1, mem_cons_of_mem p.2⟩ :=
  Quotient.inductionOn m fun l =>
    congr_arg _ <|
      congr_arg (List.cons _) <| by
        rw [List.map_pmap]; exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.eq rfl

Attached Multiset Construction for Cons Operation

Informal description

For any element $a$ of type $\alpha$ and any multiset $m$ over $\alpha$, the attached multiset of $a ::ₘ m$ (the multiset obtained by adding $a$ to $m$) is equal to the multiset obtained by: 1. Adding the pair $\langle a, h \rangle$ where $h$ is the proof that $a \in a ::ₘ m$, and 2. Mapping each element $\langle x, h_x \rangle$ in the attached multiset of $m$ to $\langle x, h'_x \rangle$ where $h'_x$ is the proof that $x \in a ::ₘ m$ derived from $h_x$ (the original proof that $x \in m$).

Multiset.erase_attach_map_val theorem

(s : Multiset α) (x : { x // x ∈ s }) : (s.attach.erase x).map (↑) = s.erase x

Full source

lemma erase_attach_map_val (s : Multiset α) (x : {x // x ∈ s}) :
    (s.attach.erase x).map (↑) = s.erase x := by
  rw [Multiset.map_erase _ val_injective, attach_map_val]

Projection of Erased Attached Multiset Equals Erased Original Multiset

Informal description

For any multiset $s$ over a type $\alpha$ and any element $x$ in the attached multiset $s.\mathrm{attach}$ (i.e., $x$ is a pair $\langle x_0, h \rangle$ where $x_0 \in s$ and $h$ is a proof of this membership), the image of the multiset $s.\mathrm{attach} \setminus \{x\}$ under the projection function $\mathrm{Subtype.val}$ is equal to the multiset $s \setminus \{x_0\}$. In other words, if we remove an element $x$ from the attached multiset $s.\mathrm{attach}$ and then project back to $\alpha$, we obtain the original multiset $s$ with one occurrence of $x_0$ removed.

Multiset.erase_attach_map theorem

 (s : Multiset α) (f : α → β) (x : { x // x ∈ s }) :
  (s.attach.erase x).map (fun j : { x // x ∈ s } ↦ f j) = (s.erase x).map f

Full source

lemma erase_attach_map (s : Multiset α) (f : α → β) (x : {x // x ∈ s}) :
    (s.attach.erase x).map (fun j : {x // x ∈ s} ↦ f j) = (s.erase x).map f := by
  simp only [← Function.comp_apply (f := f)]
  rw [← map_map, erase_attach_map_val]

Mapping after Erasure in Attached Multiset Equals Mapping after Erasure in Original Multiset

Informal description

For any multiset $s$ over a type $\alpha$, any function $f : \alpha \to \beta$, and any element $x$ in the attached multiset $s.\mathrm{attach}$ (i.e., $x$ is a pair $\langle x_0, h \rangle$ where $x_0 \in s$ and $h$ is a proof of membership), the image of the multiset $s.\mathrm{attach} \setminus \{x\}$ under the function $\lambda j, f(j)$ is equal to the image of the multiset $s \setminus \{x_0\}$ under $f$. In other words, removing an element $x$ from the attached multiset and then mapping $f$ is equivalent to removing $x_0$ from the original multiset $s$ and then mapping $f$.

Multiset.sub_eq_fold_erase theorem

(s t : Multiset α) : s - t = foldl erase s t

Full source

lemma sub_eq_fold_erase (s t : Multiset α) : s - t = foldl erase s t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => by
    show ofList (l₁.diff l₂) = foldl erase l₁ l₂
    rw [diff_eq_foldl l₁ l₂]
    symm
    exact foldl_hom _ fun x y => rfl

Multiset Subtraction as Fold of Erase Operations

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the subtraction $s - t$ is equal to the left fold of the `erase` operation over $t$ starting with $s$. That is, $s - t = \text{foldl}~\text{erase}~s~t$.

Multiset.rel_map_left theorem

{s : Multiset γ} {f : γ → α} : ∀ {t}, Rel r (s.map f) t ↔ Rel (fun a b => r (f a) b) s t

Full source

theorem rel_map_left {s : Multiset γ} {f : γ → α} :
    ∀ {t}, RelRel r (s.map f) t ↔ Rel (fun a b => r (f a) b) s t :=
  @(Multiset.induction_on s (by simp) (by simp +contextual [rel_cons_left]))

Lifting Relation through Multiset Map on Left Argument: $\text{Rel}\, r\, (s.map\, f)\, t \leftrightarrow \text{Rel}\, (r \circ f)\, s\, t$

Informal description

For any multiset $s$ over a type $\gamma$, a function $f : \gamma \to \alpha$, and a multiset $t$ over $\beta$, the relation $\text{Rel}\, r\, (s.map\, f)\, t$ holds if and only if the relation $\text{Rel}\, (\lambda a\, b, r\, (f\, a)\, b)\, s\, t$ holds. In other words, the lifted relation $\text{Rel}\, r$ between the image of $s$ under $f$ and $t$ is equivalent to the relation $\text{Rel}$ between $s$ and $t$ where $r$ is precomposed with $f$ on the first argument.

Multiset.rel_map_right theorem

{s : Multiset α} {t : Multiset γ} {f : γ → β} : Rel r s (t.map f) ↔ Rel (fun a b => r a (f b)) s t

Full source

theorem rel_map_right {s : Multiset α} {t : Multiset γ} {f : γ → β} :
    RelRel r s (t.map f) ↔ Rel (fun a b => r a (f b)) s t := by
  rw [← rel_flip, rel_map_left, ← rel_flip]; rfl

Lifting Relation through Multiset Map on Right Argument: $\text{Rel}\, r\, s\, (t.map\, f) \leftrightarrow \text{Rel}\, (r \circ (id \times f))\, s\, t$

Informal description

For any multiset $s$ over a type $\alpha$, a multiset $t$ over a type $\gamma$, and a function $f : \gamma \to \beta$, the relation $\text{Rel}\, r\, s\, (t.map\, f)$ holds if and only if the relation $\text{Rel}\, (\lambda a\, b, r\, a\, (f\, b))\, s\, t$ holds. In other words, the lifted relation $\text{Rel}\, r$ between $s$ and the image of $t$ under $f$ is equivalent to the relation $\text{Rel}$ between $s$ and $t$ where $r$ is postcomposed with $f$ on the second argument.

Multiset.rel_map theorem

 {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ} :
  Rel p (s.map f) (t.map g) ↔ Rel (fun a b => p (f a) (g b)) s t

Full source

theorem rel_map {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ} :
    RelRel p (s.map f) (t.map g) ↔ Rel (fun a b => p (f a) (g b)) s t :=
  rel_map_left.trans rel_map_right

Lifting Relation through Multiset Maps: $\text{Rel}\, p\, (s.map\, f)\, (t.map\, g) \leftrightarrow \text{Rel}\, (p \circ (f \times g))\, s\, t$

Informal description

For any multisets $s$ over type $\alpha$ and $t$ over type $\beta$, and functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$, the relation $\text{Rel}\, p\, (s.map\, f)\, (t.map\, g)$ holds if and only if the relation $\text{Rel}\, (\lambda a\, b, p\, (f\, a)\, (g\, b))\, s\, t$ holds. In other words, the lifted relation $\text{Rel}\, p$ between the images of $s$ under $f$ and $t$ under $g$ is equivalent to the relation $\text{Rel}$ between $s$ and $t$ where $p$ is composed with $f$ and $g$ on its arguments.

Multiset.map_eq_map theorem

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

Full source

theorem map_eq_map {f : α → β} (hf : Function.Injective f) {s t : Multiset α} :
    s.map f = t.map f ↔ s = t := by
  rw [← rel_eq, ← rel_eq, rel_map]
  simp only [hf.eq_iff]

Injectivity of Multiset Map for Injective Functions: $s.\text{map}\, f = t.\text{map}\, f \leftrightarrow s = t$

Informal description

Let $f : \alpha \to \beta$ be an injective function. For any multisets $s$ and $t$ over $\alpha$, the images of $s$ and $t$ under $f$ are equal if and only if $s$ and $t$ are equal as multisets. In other words, $f$ induces an injective map on multisets.

Multiset.map_injective theorem

{f : α → β} (hf : Function.Injective f) : Function.Injective (Multiset.map f)

Full source

theorem map_injective {f : α → β} (hf : Function.Injective f) :
    Function.Injective (Multiset.map f) := fun _x _y => (map_eq_map hf).1

Injectivity of Multiset Map for Injective Functions

Informal description

For any injective function $f : \alpha \to \beta$, the induced map on multisets $\text{map}\, f : \text{Multiset}\, \alpha \to \text{Multiset}\, \beta$ is also injective. That is, if $\text{map}\, f\, s = \text{map}\, f\, t$ for two multisets $s$ and $t$ over $\alpha$, then $s = t$.

Multiset.map_mk_eq_map_mk_of_rel theorem

{r : α → α → Prop} {s t : Multiset α} (hst : s.Rel r t) : s.map (Quot.mk r) = t.map (Quot.mk r)

Full source

theorem map_mk_eq_map_mk_of_rel {r : α → α → Prop} {s t : Multiset α} (hst : s.Rel r t) :
    s.map (Quot.mk r) = t.map (Quot.mk r) :=
  Rel.recOn hst rfl fun hab _hst ih => by simp [ih, Quot.sound hab]

Equality of Quotient Images for Related Multisets

Informal description

For any relation $r$ on a type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, if there exists a relation-preserving bijection between $s$ and $t$ (i.e., $s$ and $t$ are related under the lifted relation $\text{Rel}\,r$), then the images of $s$ and $t$ under the quotient map $\text{Quot.mk}\,r$ are equal as multisets.

Multiset.exists_multiset_eq_map_quot_mk theorem

{r : α → α → Prop} (s : Multiset (Quot r)) : ∃ t : Multiset α, s = t.map (Quot.mk r)

Full source

theorem exists_multiset_eq_map_quot_mk {r : α → α → Prop} (s : Multiset (Quot r)) :
    ∃ t : Multiset α, s = t.map (Quot.mk r) :=
  Multiset.induction_on s ⟨0, rfl⟩ fun a _s ⟨t, ht⟩ =>
    Quot.inductionOn a fun a => ht.symm ▸ ⟨a ::ₘ t, (map_cons _ _ _).symm⟩

Lifting of Multisets to Quotient via Equivalence Relation

Informal description

For any equivalence relation $r$ on a type $\alpha$ and any multiset $s$ of equivalence classes (quotients) under $r$, there exists a multiset $t$ of elements of $\alpha$ such that $s$ is equal to the image of $t$ under the quotient map $\text{Quot.mk}\,r$.

Multiset.induction_on_multiset_quot theorem

 {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)) :
  (∀ s : Multiset α, p (s.map (Quot.mk r))) → p s

Full source

theorem induction_on_multiset_quot {r : α → α → Prop} {p : Multiset (Quot r) → Prop}
    (s : Multiset (Quot r)) : (∀ s : Multiset α, p (s.map (Quot.mk r))) → p s :=
  match s, exists_multiset_eq_map_quot_mk s with
  | _, ⟨_t, rfl⟩ => fun h => h _

Induction Principle for Multisets of Quotients via Lifting from Base Type

Informal description

Let $r$ be a relation on a type $\alpha$ and $p$ be a predicate on multisets of equivalence classes under $r$. For any multiset $s$ of such equivalence classes, if $p$ holds for the image of every multiset $t$ of $\alpha$ under the quotient map $\text{Quot.mk}\,r$, then $p$ holds for $s$.

Multiset.Nodup.of_map theorem

(f : α → β) : Nodup (map f s) → Nodup s

Full source

theorem Nodup.of_map (f : α → β) : Nodup (map f s) → Nodup s :=
  Quot.induction_on s fun _ => List.Nodup.of_map f

Original Multiset is Duplicate-Free if Mapped Multiset is Duplicate-Free

Informal description

For any function $f : \alpha \to \beta$ and any multiset $s$ over $\alpha$, if the image multiset $\mathrm{map}\,f\,s$ has no duplicate elements, then the original multiset $s$ also has no duplicate elements.

Multiset.Nodup.map_on theorem

{f : α → β} : (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Nodup s → Nodup (map f s)

Full source

theorem Nodup.map_on {f : α → β} :
    (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Nodup s → Nodup (map f s) :=
  Quot.induction_on s fun _ => List.Nodup.map_on

Preservation of Distinctness under Injective Mapping on Multisets

Informal description

Let $f : \alpha \to \beta$ be a function and $s$ be a multiset over $\alpha$. If $f$ is injective on the elements of $s$ (i.e., for any $x, y \in s$, $f(x) = f(y)$ implies $x = y$) and $s$ has no duplicate elements, then the image multiset $\mathrm{map}\,f\,s$ also has no duplicate elements.

Multiset.Nodup.map theorem

{f : α → β} {s : Multiset α} (hf : Injective f) : Nodup s → Nodup (map f s)

Full source

theorem Nodup.map {f : α → β} {s : Multiset α} (hf : Injective f) : Nodup s → Nodup (map f s) :=
  Nodup.map_on fun _ _ _ _ h => hf h

Injective Function Preserves Distinctness in Multiset Mapping

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s$ be a multiset over $\alpha$. If $s$ has no duplicate elements, then the image multiset $\mathrm{map}\,f\,s$ also has no duplicate elements.

Multiset.nodup_map_iff_of_inj_on theorem

{f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) : Nodup (map f s) ↔ Nodup s

Full source

theorem nodup_map_iff_of_inj_on {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) :
    NodupNodup (map f s) ↔ Nodup s :=
  ⟨Nodup.of_map _, fun h => h.map_on d⟩

Equivalence of Distinctness in Multiset and Its Image under Injective-on-Elements Function

Informal description

Let $f : \alpha \to \beta$ be a function and $s$ be a multiset over $\alpha$. If $f$ is injective on the elements of $s$ (i.e., for any $x, y \in s$, $f(x) = f(y)$ implies $x = y$), then the image multiset $\mathrm{map}\,f\,s$ has no duplicate elements if and only if $s$ has no duplicate elements.

Multiset.nodup_map_iff_of_injective theorem

{f : α → β} (d : Function.Injective f) : Nodup (map f s) ↔ Nodup s

Full source

theorem nodup_map_iff_of_injective {f : α → β} (d : Function.Injective f) :
    NodupNodup (map f s) ↔ Nodup s :=
  ⟨Nodup.of_map _, fun h => h.map d⟩

Distinctness Preservation under Injective Mapping: $\mathrm{Nodup}(\mathrm{map}\,f\,s) \leftrightarrow \mathrm{Nodup}(s)$

Informal description

Let $f : \alpha \to \beta$ be an injective function and $s$ be a multiset over $\alpha$. Then the image multiset $\mathrm{map}\,f\,s$ has no duplicate elements if and only if $s$ has no duplicate elements.

Multiset.inj_on_of_nodup_map theorem

{f : α → β} {s : Multiset α} : Nodup (map f s) → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y

Full source

theorem inj_on_of_nodup_map {f : α → β} {s : Multiset α} :
    Nodup (map f s) → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
  Quot.induction_on s fun _ => List.inj_on_of_nodup_map

Injectivity from Distinctness of Mapped Multiset

Informal description

For any function $f : \alpha \to \beta$ and any multiset $s$ over $\alpha$, if the multiset $\mathrm{map}\,f\,s$ has no duplicates, then $f$ is injective on the elements of $s$, i.e., for any $x, y \in s$, $f(x) = f(y)$ implies $x = y$.

Multiset.nodup_map_iff_inj_on theorem

{f : α → β} {s : Multiset α} (d : Nodup s) : Nodup (map f s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y

Full source

theorem nodup_map_iff_inj_on {f : α → β} {s : Multiset α} (d : Nodup s) :
    NodupNodup (map f s) ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
  ⟨inj_on_of_nodup_map, fun h => d.map_on h⟩

Distinctness of Mapped Multiset Equivalence to Injectivity on Elements

Informal description

Let $f : \alpha \to \beta$ be a function and $s$ be a multiset over $\alpha$ with no duplicate elements. Then the image multiset $\mathrm{map}\,f\,s$ has no duplicates if and only if $f$ is injective on the elements of $s$, i.e., for any $x, y \in s$, $f(x) = f(y)$ implies $x = y$.

Multiset.Nodup.pmap theorem

 {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H} (hf : ∀ a ha b hb, f a ha = f b hb → a = b) :
  Nodup s → Nodup (pmap f s H)

Full source

theorem Nodup.pmap {p : α → Prop} {f : ∀ a, p a → β} {s : Multiset α} {H}
    (hf : ∀ a ha b hb, f a ha = f b hb → a = b) : Nodup s → Nodup (pmap f s H) :=
  Quot.induction_on s (fun _ _ => List.Nodup.pmap hf) H

Preservation of Distinctness under Partial Mapping of Multisets

Informal description

Let $p : \alpha \to \mathrm{Prop}$ be a predicate and $f : \forall a, p(a) \to \beta$ be a dependent function. For any multiset $s$ over $\alpha$ with no duplicates, if $f$ is injective in the sense that $f(a, h_a) = f(b, h_b)$ implies $a = b$ for any $a, b \in \alpha$ and any proofs $h_a : p(a)$, $h_b : p(b)$, then the multiset obtained by applying $f$ to each element of $s$ (denoted $\mathrm{pmap}\,f\,s\,H$) also has no duplicates.

Multiset.nodup_attach theorem

{s : Multiset α} : Nodup (attach s) ↔ Nodup s

Full source

@[simp]
theorem nodup_attach {s : Multiset α} : NodupNodup (attach s) ↔ Nodup s :=
  Quot.induction_on s fun _ => List.nodup_attach

Equivalence of Distinctness Between Multiset and Its Attached Version

Informal description

For any multiset $s$ over a type $\alpha$, the attached multiset (where each element is paired with its membership proof) has no duplicates if and only if the original multiset $s$ has no duplicates.

Multiset.map_eq_map_of_bij_of_nodup theorem

 (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β} (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β)
  (hi : ∀ a ha, i a ha ∈ t) (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
  (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : s.map f = t.map g

Full source

theorem map_eq_map_of_bij_of_nodup (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β}
    (hs : s.Nodup) (ht : t.Nodup) (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)
    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : s.map f = t.map g := by
  have : t = s.attach.map fun x => i x.1 x.2 := by
    rw [ht.ext]
    · aesop
    · exact hs.attach.map fun x y hxy ↦ Subtype.ext <| i_inj _ x.2 _ y.2 hxy
  calc
    s.map f = s.pmap (fun x _ => f x) fun _ => id := by rw [pmap_eq_map]
    _ = s.attach.map fun x => f x.1 := by rw [pmap_eq_map_attach]
    _ = t.map g := by rw [this, Multiset.map_map]; exact map_congr rfl fun x _ => h _ _

Equality of Multiset Images under Bijective Correspondence and Function Agreement

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \gamma$ be functions, and let $s$ and $t$ be duplicate-free multisets over $\alpha$ and $\beta$, respectively. Suppose there exists a bijection $i$ between the elements of $s$ and $t$ such that: 1. For every $a \in s$ with proof $ha$, $i(a, ha) \in t$, 2. $i$ is injective: if $i(a_1, ha_1) = i(a_2, ha_2)$, then $a_1 = a_2$, 3. $i$ is surjective: for every $b \in t$, there exists $a \in s$ with proof $ha$ such that $i(a, ha) = b$, 4. The functions agree on corresponding elements: $f(a) = g(i(a, ha))$ for all $a \in s$ with proof $ha$. Then the image multisets satisfy $\mathrm{map}\,f\,s = \mathrm{map}\,g\,t$.

Mathlib.Data.Multiset.MapFold

Main definitions

TODO