English
Suppose you have two multisets s and t that are Nodup, and a family of elements i(a) in β corresponding to each a ∈ s, along with compatibility data linking f and g through i. If f is determined by a bijection i between s and t that preserves elements and witnesses, then s.map f equals t.map g.
Русский
Пусть s и t — две безповторные подмножества; имеется семейство элементов i(a) в β и соответствия между f и g через i, задающее биекцию между элементами; тогда совпадение отображений приводит к равенству образов: s.map f = t.map g.
LaTeX
$$$\\forall f:\\alpha\\to\\gamma,\\;\\forall g:\\beta\\to\\gamma,\\;\\forall s t:\\mathrm{Multiset}\\;\\alpha\\;\\mathrm{etc.}\\;\\Big(\\operatorname{Nodup}(s) \\wedge \\operatorname{Nodup}(t) \\wedge \\cdots\\Big) \\Rightarrow s.map f = t.map g.$$$
Lean4
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 _ _
