English
For Quot r, there is an induction principle: to prove a property p on Multiset (Quot r) it suffices to prove p on the image of every s under Quot.mk r.
Русский
Для Quot r существует принцип индукции: чтобы доказать свойство p на Multiset (Quot r), достаточно доказать p на образе каждого s под Quot.mk r.
LaTeX
$$$\\forall {r : α \\to α \\to Prop},\\ {p : \\mathrm{Multiset}(\\mathrm{Quot} r) \\to \\mathrm{Prop}} ,\\forall s : \\mathrm{Multiset}(\\mathrm{Quot} r),\\ (\\\\forall s : \\mathrm{Multiset}\\\\ α,\\\\ p (\\\\mathrm{Multiset.map}(\\\\mathrm{Quot.mk} r) s)) \\\\to p\\\\ s.$$$
Lean4
theorem exists_multiset_eq_map_quot_mk {r : α → α → Prop} (s : Multiset (Quot r)) :
∃ t : Multiset α, s = t.map (Quot.mk r) :=
Multiset.induction_on s ⟨0, rfl⟩ fun a _s ⟨t, ht⟩ =>
Quot.inductionOn a fun a => ht.symm ▸ ⟨a ::ₘ t, (map_cons _ _ _).symm⟩
