# Mapping and folding multisets #

## Main definitions #

- `Multiset.map`: `map f s` applies `f` to each element of `s`.
- `Multiset.foldl`: `foldl f b s` picks elements out of `s` and applies `f (f ... b x₁) x₂`.
- `Multiset.foldr`: `foldr f b s` picks elements out of `s` and applies `f x₁ (f ... x₂ b)`.

## TODO #

Many lemmas about `Multiset.map` are proven in `Mathlib/Data/Multiset/Filter.lean`: should we switch the import direction?

### `Multiset.map` #

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

`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`.

Equations

- Multiset.map f s = Quot.liftOn s (fun (l : List α) => ↑(List.map f l)) ⋯

Instances For

source
theorem Multiset.map_congr {α : Type u_1} {β : Type v} {f g : α → β} {s t : Multiset α} :
s = t → (∀ x ∈ t, f x = g x) → map f s = map g t
source
theorem Multiset.map_hcongr {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → β} {f' : α → β'} (h : β = β') (hf : ∀ a ∈ m, f a ≍ f' a) :
map f m ≍ map f' m
source
theorem Multiset.forall_mem_map_iff {α : Type u_1} {β : Type v} {f : α → β} {p : β → Prop} {s : Multiset α} :
(∀ y ∈ map f s, p y) ↔ ∀ x ∈ s, p (f x)
source
@[simp]
theorem Multiset.map_coe {α : Type u_1} {β : Type v} (f : α → β) (l : List α) :
map f ↑l = ↑(List.map f l)
source
@[simp]
theorem Multiset.map_zero {α : Type u_1} {β : Type v} (f : α → β) :
map f 0 = 0
source
@[simp]
theorem Multiset.map_cons {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α) :
map f (a ::ₘ s) = f a ::ₘ map f s
source
theorem Multiset.map_comp_cons {α : Type u_1} {β : Type v} (f : α → β) (t : α) :
map f ∘ cons t = cons (f t) ∘ map f
source
@[simp]
theorem Multiset.map_singleton {α : Type u_1} {β : Type v} (f : α → β) (a : α) :
map f {a} = {f a}
source
@[simp]
theorem Multiset.map_replicate {α : Type u_1} {β : Type v} (f : α → β) (k : ℕ) (a : α) :
map f (replicate k a) = replicate k (f a)
source
@[simp]
theorem Multiset.map_add {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α) :
map f (s + t) = map f s + map f t
source
instance Multiset.canLift {α : Type u_1} {β : Type v} (c : β → α) (p : α → Prop) [CanLift α β c p] :
CanLift (Multiset α) (Multiset β) (map c) fun (s : Multiset α) => ∀ x ∈ s, p x

If each element of `s : Multiset α` can be lifted to `β`, then `s` can be lifted to `Multiset β`.

source
@[simp]
theorem Multiset.mem_map {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α} :
b ∈ map f s ↔ ∃ a ∈ s, f a = b
source
@[simp]
theorem Multiset.card_map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) :
(map f s).card = s.card
source
@[simp]
theorem Multiset.map_eq_zero {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} :
map f s = 0 ↔ s = 0
source
theorem Multiset.mem_map_of_mem {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) :
f a ∈ map f s
source
theorem Multiset.map_eq_singleton {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} {b : β} :
map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b
source
theorem Multiset.map_eq_cons {α : Type u_1} {β : Type v} [DecidableEq α] (f : α → β) (s : Multiset α) (t : Multiset β) (b : β) :
(∃ a ∈ s, f a = b ∧ map f (s.erase a) = t) ↔ map f s = b ::ₘ t
source
@[simp]
theorem Multiset.mem_map_of_injective {α : Type u_1} {β : Type v} {f : α → β} (H : Function.Injective f) {a : α} {s : Multiset α} :
f a ∈ map f s ↔ a ∈ s
source
@[simp]
theorem Multiset.map_map {α : Type u_1} {β : Type v} {γ : Type u_2} (g : β → γ) (f : α → β) (s : Multiset α) :
map g (map f s) = map (g ∘ f) s
source
theorem Multiset.map_id {α : Type u_1} (s : Multiset α) :
map id s = s
source
@[simp]
theorem Multiset.map_id' {α : Type u_1} (s : Multiset α) :
map (fun (x : α) => x) s = s
source
theorem Multiset.map_const {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) :
map (Function.const α b) s = replicate s.card b
source
@[simp]
theorem Multiset.map_const' {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) :
map (fun (x : α) => b) s = replicate s.card b
source
theorem Multiset.eq_of_mem_map_const {α : Type u_1} {β : Type v} {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) ↑l) :
b₁ = b₂
source
@[simp]
theorem Multiset.map_le_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s ≤ t) :
map f s ≤ map f t
source
@[simp]
theorem Multiset.map_lt_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s < t) :
map f s < map f t
source
theorem Multiset.map_mono {α : Type u_1} {β : Type v} (f : α → β) :
Monotone (map f)
source
theorem Multiset.map_strictMono {α : Type u_1} {β : Type v} (f : α → β) :
StrictMono (map f)
source
@[simp]
theorem Multiset.map_subset_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (H : s ⊆ t) :
map f s ⊆ map f t
source
theorem Multiset.map_erase {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (hf : Function.Injective f) (x : α) (s : Multiset α) :
map f (s.erase x) = (map f s).erase (f x)
source
theorem Multiset.map_erase_of_mem {α : Type u_1} {β : Type v} [DecidableEq α] [DecidableEq β] (f : α → β) (s : Multiset α) {x : α} (h : x ∈ s) :
map f (s.erase x) = (map f s).erase (f x)
source
theorem Multiset.map_surjective_of_surjective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Surjective f) :
Function.Surjective (map f)

### `Multiset.fold` #

source
def Multiset.foldl {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) :
β

`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₁`.

Equations

- Multiset.foldl f b s = Quot.liftOn s (fun (l : List α) => List.foldl f b l) ⋯

Instances For

source
@[simp]
theorem Multiset.foldl_zero {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) :
foldl f b 0 = b
source
@[simp]
theorem Multiset.foldl_cons {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (a : α) (s : Multiset α) :
foldl f b (a ::ₘ s) = foldl f (f b a) s
source
@[simp]
theorem Multiset.foldl_add {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s t : Multiset α) :
foldl f b (s + t) = foldl f (foldl f b s) t
source
def Multiset.foldr {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) :
β

`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)`.

Equations

- Multiset.foldr f b s = Quot.liftOn s (fun (l : List α) => List.foldr f b l) ⋯

Instances For

source
@[simp]
theorem Multiset.foldr_zero {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) :
foldr f b 0 = b
source
@[simp]
theorem Multiset.foldr_cons {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (a : α) (s : Multiset α) :
foldr f b (a ::ₘ s) = f a (foldr f b s)
source
@[simp]
theorem Multiset.foldr_singleton {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (a : α) :
foldr f b {a} = f a b
source
@[simp]
theorem Multiset.foldr_add {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s t : Multiset α) :
foldr f b (s + t) = foldr f (foldr f b t) s
source
@[simp]
theorem Multiset.coe_foldr {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) :
foldr f b ↑l = List.foldr f b l
source
@[simp]
theorem Multiset.coe_foldl {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (l : List α) :
foldl f b ↑l = List.foldl f b l
source
theorem Multiset.coe_foldr_swap {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (l : List α) :
foldr f b ↑l = List.foldl (fun (x : β) (y : α) => f y x) b l
source
theorem Multiset.foldr_swap {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (s : Multiset α) :
foldr f b s = foldl (fun (x : β) (y : α) => f y x) b s
source
theorem Multiset.foldl_swap {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) (s : Multiset α) :
foldl f b s = foldr (fun (x : α) (y : β) => f y x) b s
source
theorem Multiset.foldr_induction' {α : Type u_1} {β : Type v} (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)
source
theorem Multiset.foldr_induction {α : Type u_1} (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)
source
theorem Multiset.foldl_induction' {α : Type u_1} {β : Type v} (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)
source
theorem Multiset.foldl_induction {α : Type u_1} (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)

### Map for partial functions #

source
theorem Multiset.pmap_eq_map {α : Type u_1} {β : Type v} (p : α → Prop) (f : α → β) (s : Multiset α) (H : ∀ a ∈ s, p a) :
pmap (fun (a : α) (x : p a) => f a) s H = map f s
source
theorem Multiset.map_pmap {α : Type u_1} {β : Type v} {γ : Type u_2} {p : α → Prop} (g : β → γ) (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) :
map g (pmap f s H) = pmap (fun (a : α) (h : p a) => g (f a h)) s H
source
theorem Multiset.pmap_eq_map_attach {α : Type u_1} {β : Type v} {p : α → Prop} (f : (a : α) → p a → β) (s : Multiset α) (H : ∀ a ∈ s, p a) :
pmap f s H = map (fun (x : { x : α // x ∈ s }) => f ↑x ⋯) s.attach
source
@[simp]
theorem Multiset.attach_map_val' {α : Type u_1} {β : Type v} (s : Multiset α) (f : α → β) :
map (fun (i : { x : α // x ∈ s }) => f ↑i) s.attach = map f s
source
@[simp]
theorem Multiset.attach_map_val {α : Type u_1} (s : Multiset α) :
map Subtype.val s.attach = s
source
theorem Multiset.attach_cons {α : Type u_1} (a : α) (m : Multiset α) :
(a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ map (fun (p : { x : α // x ∈ m }) => ⟨↑p, ⋯⟩) m.attach
source
theorem Multiset.erase_attach_map_val {α : Type u_1} [DecidableEq α] (s : Multiset α) (x : { x : α // x ∈ s }) :
map Subtype.val (s.attach.erase x) = s.erase ↑x
source
theorem Multiset.erase_attach_map {α : Type u_1} {β : Type v} [DecidableEq α] (s : Multiset α) (f : α → β) (x : { x : α // x ∈ s }) :
map (fun (j : { x : α // x ∈ s }) => f ↑j) (s.attach.erase x) = map f (s.erase ↑x)

### Subtraction #

source
theorem Multiset.sub_eq_fold_erase {α : Type u_1} [DecidableEq α] (s t : Multiset α) :
s - t = foldl erase s t

### Lift a relation to `Multiset`s #

source
theorem Multiset.rel_map_left {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset γ} {f : γ → α} {t : Multiset β} :
Rel r (map f s) t ↔ Rel (fun (a : γ) (b : β) => r (f a) b) s t
source
theorem Multiset.rel_map_right {α : Type u_1} {β : Type v} {γ : Type u_2} {r : α → β → Prop} {s : Multiset α} {t : Multiset γ} {f : γ → β} :
Rel r s (map f t) ↔ Rel (fun (a : α) (b : γ) => r a (f b)) s t
source
theorem Multiset.rel_map {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β} {f : α → γ} {g : β → δ} :
Rel p (map f s) (map g t) ↔ Rel (fun (a : α) (b : β) => p (f a) (g b)) s t
source
theorem Multiset.map_eq_map {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) {s t : Multiset α} :
map f s = map f t ↔ s = t
source
theorem Multiset.map_injective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) :
Function.Injective (map f)
source
theorem Multiset.map_mk_eq_map_mk_of_rel {α : Type u_1} {r : α → α → Prop} {s t : Multiset α} (hst : Rel r s t) :
map (Quot.mk r) s = map (Quot.mk r) t
source
theorem Multiset.exists_multiset_eq_map_quot_mk {α : Type u_1} {r : α → α → Prop} (s : Multiset (Quot r)) :
∃ (t : Multiset α), s = map (Quot.mk r) t
source
theorem Multiset.induction_on_multiset_quot {α : Type u_1} {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)) :
(∀ (s : Multiset α), p (map (Quot.mk r) s)) → p s
source
theorem Multiset.Nodup.of_map {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → β) :
(Multiset.map f s).Nodup → s.Nodup
source
theorem Multiset.Nodup.map_on {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} :
(∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → s.Nodup → (Multiset.map f s).Nodup
source
theorem Multiset.Nodup.map {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} (hf : Function.Injective f) :
s.Nodup → (Multiset.map f s).Nodup
source
theorem Multiset.nodup_map_iff_of_inj_on {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} (d : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) :
(map f s).Nodup ↔ s.Nodup
source
theorem Multiset.nodup_map_iff_of_injective {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} (d : Function.Injective f) :
(map f s).Nodup ↔ s.Nodup
source
theorem Multiset.inj_on_of_nodup_map {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} :
(map f s).Nodup → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
source
theorem Multiset.nodup_map_iff_inj_on {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} (d : s.Nodup) :
(map f s).Nodup ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
source
theorem Multiset.Nodup.pmap {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a} (hf : ∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) :
s.Nodup → (Multiset.pmap f s H).Nodup
source
@[simp]
theorem Multiset.nodup_attach {α : Type u_1} {s : Multiset α} :
s.attach.Nodup ↔ s.Nodup
source
theorem Multiset.Nodup.attach {α : Type u_1} {s : Multiset α} :
s.Nodup → s.attach.Nodup

Alias of the reverse direction of `Multiset.nodup_attach`.

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