English
Rel_map_left establishes an equivalence form for the left-mapped relation: Rel r (s.map f) t is equivalent to Rel (λ a b, r (f a) b) s t, holding uniformly for all s, f, t.
Русский
Rel_map_left устанавливает эквивалентную форму для левого отображения отношения: 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,\\\\ (Rel \\\\ r (s.\\\\map f) t) \\\\iff \\\\ Rel (\\\\lambda a b. \\\\ r (f a) b) s t.$$$
Lean4
theorem rel_map_right {s : Multiset α} {t : Multiset γ} {f : γ → β} :
Rel r s (t.map f) ↔ Rel (fun a b => r a (f b)) s t := by rw [← rel_flip, rel_map_left, ← rel_flip]; rfl
