English
For multisets s of γ and a function f: γ → α, Rel r (s.map f) t is equivalent to Rel (λ a b, r (f a) b) s t for all t, i.e., the relation is preserved under left-mapping.
Русский
Для мультимножества s из γ и функции f: γ → α отношение Rel r между s.map f и t эквивалентно Rel (λ a b, r (f a) b) между s и t.
LaTeX
$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\gamma,\\\\forall f:\\\\gamma\\\\to\\\\alpha,\\\\forall t,\\\\ \\mathrm{Rel}\\\\ r (s.\\\\map f) t \\\\iff \\\\mathrm{Rel}\\\\ (\\\\lambda a b.\\\\ r (f a) b) s t.$$$
Lean4
theorem rel_map_left {s : Multiset γ} {f : γ → α} : ∀ {t}, Rel r (s.map f) t ↔ Rel (fun a b => r (f a) b) s t :=
@(Multiset.induction_on s (by simp) (by simp +contextual [rel_cons_left]))
