English
Let s be a finite set of indices γ, f : γ → Multiset β, g : β → α be injective, and α, β be types with decidable equality. Then map g distributes over the finite sup: map g (s.sup f) = s.sup (map g ∘ f).
Русский
Пусть s — конечный набор индексов γ, f : γ → Multiset β, g : β → α — инъекция, тогда отображение по g сохраняет операцию объединения: map g (s.sup f) = s.sup (map g ∘ f).
LaTeX
$$$\\mathrm{map}\\ g\\ (s.\\mathrm{sup}\\ f) = s.\\mathrm{sup}\\ (\\mathrm{map}\\ g \\circ f).$$$
Lean4
theorem map_finset_sup [DecidableEq α] [DecidableEq β] (s : Finset γ) (f : γ → Multiset β) (g : β → α)
(hg : Function.Injective g) : map g (s.sup f) = s.sup (map g ∘ f) :=
Finset.comp_sup_eq_sup_comp _ (fun _ _ => map_union hg) (map_zero _)
