English
For multisets s of α and t of β, and functions f: α→γ and g: β→δ, Rel p (s.map f) (t.map g) is equivalent to Rel (λ a b, p (f a) (g b)) s t.
Русский
Для мультимножества s из α и t из β и функций f: α→γ, g: β→δ, Rel p (s.map f) (t.map g) эквивалентно Rel (λ a b, p (f a) (g b)) s t.
LaTeX
$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\alpha,\\\\forall t:\\\\mathrm{Multiset}\\\\ \\beta,\\\\forall f:\\\\alpha\\\\to\\\\gamma,\\\\forall g:\\\\beta\\\\to\\\\delta,\\\\ (Rel p (s.map f) (t.map g)) \\\\iff \\\\ Rel (\\\\lambda a b.\\\\ p (f a) (g b)) s t.$$$
Lean4
theorem rel_map {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 :=
rel_map_left.trans rel_map_right
