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: should we switch the import direction?

Multiset.map

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)) ⋯

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

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

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)

@[simp]

theorem Multiset.map_coe {α : Type u_1} {β : Type v} (f : α → β) (l : List α) : map f ↑l = ↑(List.map f l)

@[simp]

theorem Multiset.map_zero {α : Type u_1} {β : Type v} (f : α → β) : map f 0 = 0

@[simp]

theorem Multiset.map_cons {α : Type u_1} {β : Type v} (f : α → β) (a : α) (s : Multiset α) : map f (a ::ₘ s) = f a ::ₘ map f s

theorem Multiset.map_comp_cons {α : Type u_1} {β : Type v} (f : α → β) (t : α) : map f ∘ cons t = cons (f t) ∘ map f

@[simp]

theorem Multiset.map_singleton {α : Type u_1} {β : Type v} (f : α → β) (a : α) : map f {a} = {f a}

@[simp]

theorem Multiset.map_replicate {α : Type u_1} {β : Type v} (f : α → β) (k : ℕ) (a : α) : map f (replicate k a) = replicate k (f a)

@[simp]

theorem Multiset.map_add {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α) : map f (s + t) = map f s + map f t

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

@[simp]

theorem Multiset.mem_map {α : Type u_1} {β : Type v} {f : α → β} {b : β} {s : Multiset α} : b ∈ map f s ↔ ∃ a ∈ s, f a = b

@[simp]

theorem Multiset.card_map {α : Type u_1} {β : Type v} (f : α → β) (s : Multiset α) : (map f s).card = s.card

@[simp]

theorem Multiset.map_eq_zero {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β} : map f s = 0 ↔ s = 0

theorem Multiset.mem_map_of_mem {α : Type u_1} {β : Type v} (f : α → β) {a : α} {s : Multiset α} (h : a ∈ s) : f a ∈ map f s

theorem Multiset.map_eq_singleton {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α} {b : β} : map f s = {b} ↔ ∃ (a : α), s = {a} ∧ f a = b

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

@[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

@[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

theorem Multiset.map_id {α : Type u_1} (s : Multiset α) : map id s = s

@[simp]

theorem Multiset.map_id' {α : Type u_1} (s : Multiset α) : map (fun (x : α) => x) s = s

theorem Multiset.map_const {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : map (Function.const α b) s = replicate s.card b

@[simp]

theorem Multiset.map_const' {α : Type u_1} {β : Type v} (s : Multiset α) (b : β) : map (fun (x : α) => b) s = replicate s.card b

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₂

@[simp]

theorem Multiset.map_le_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s ≤ t) : map f s ≤ map f t

@[simp]

theorem Multiset.map_lt_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (h : s < t) : map f s < map f t

theorem Multiset.map_mono {α : Type u_1} {β : Type v} (f : α → β) : Monotone (map f)

theorem Multiset.map_strictMono {α : Type u_1} {β : Type v} (f : α → β) : StrictMono (map f)

@[simp]

theorem Multiset.map_subset_map {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α} (H : s ⊆ t) : map f s ⊆ map f t

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)

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)

theorem Multiset.map_surjective_of_surjective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Surjective f) : Function.Surjective (map f)

Multiset.fold

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) ⋯

@[simp]

theorem Multiset.foldl_zero {α : Type u_1} {β : Type v} (f : β → α → β) [RightCommutative f] (b : β) : foldl f b 0 = b

@[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

@[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

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) ⋯

@[simp]

theorem Multiset.foldr_zero {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) : foldr f b 0 = b

@[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)

@[simp]

theorem Multiset.foldr_singleton {α : Type u_1} {β : Type v} (f : α → β → β) [LeftCommutative f] (b : β) (a : α) : foldr f b {a} = f a b

@[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

@[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

@[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

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

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

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

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)

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)

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)

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

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

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

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

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

@[simp]

theorem Multiset.attach_map_val {α : Type u_1} (s : Multiset α) : map Subtype.val s.attach = s

theorem Multiset.attach_cons {α : Type u_1} (a : α) (m : Multiset α) : (a ::ₘ m).attach = ⟨a, ⋯⟩ ::ₘ map (fun (p : { x : α // x ∈ m }) => ⟨↑p, ⋯⟩) m.attach

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

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

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

Lift a relation to Multisets

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

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

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

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

theorem Multiset.map_injective {α : Type u_1} {β : Type v} {f : α → β} (hf : Function.Injective f) : Function.Injective (map f)

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

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

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

theorem Multiset.Nodup.of_map {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → β) : (Multiset.map f s).Nodup → s.Nodup

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

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

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

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

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

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

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

@[simp]

theorem Multiset.nodup_attach {α : Type u_1} {s : Multiset α} : s.attach.Nodup ↔ s.Nodup

theorem Multiset.Nodup.attach {α : Type u_1} {s : Multiset α} : s.Nodup → s.attach.Nodup

Alias of the reverse direction of Multiset.nodup_attach.

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