English
Every multiset of quotients s : Multiset (Quot r) can be represented as the image of a multiset t under the quotient MK, i.e., there exists t with s = map (Quot.mk r) t.
Русский
Любое мультимножество частично упрощённых элементов Quot r можно представить как отображение некоторого мультимножества t через отображение Quot.mk r, то есть существует t такое, что s = map (Quot.mk r) t.
LaTeX
$$$\\forall {r : α \\to α \\to Prop},\\; (s : \\mathrm{Multiset}(\\mathrm{Quot} r))\\;:\\\\Exists t : \\mathrm{Multiset}\\\\ \\alpha,\\\\ s = \\mathrm{Multiset.map}(\\\\mathrm{Quot.mk} r) t$$$
Lean4
theorem map_mk_eq_map_mk_of_rel {r : α → α → Prop} {s t : Multiset α} (hst : s.Rel r t) :
s.map (Quot.mk r) = t.map (Quot.mk r) :=
Rel.recOn hst rfl fun hab _hst ih => by simp [ih, Quot.sound hab]
