English
Equivalent to induction on Multiset (Quot r): to prove a property p on s : Multiset (Quot r) it suffices to show p on s.map (Quot.mk r) for all s : Multiset α.
Русский
Эквивалентно индукции по Multiset (Quot r): чтобы доказать свойство p для s : Multiset (Quot r), достаточно показать p на s.map (Quot.mk r) для всех s : Multiset α.
LaTeX
$$$\\forall {r : α \\to α \\to Prop}, {p : Multiset(\\ Quot r) \\to Prop} , (\\forall s : \\ Multiset α, p (\\\\mathrm{Multiset.map}(\\\\mathrm{Quot.mk} r) s)) \\\\to p s$$$
Lean4
theorem induction_on_multiset_quot {r : α → α → Prop} {p : Multiset (Quot r) → Prop} (s : Multiset (Quot r)) :
(∀ s : Multiset α, p (s.map (Quot.mk r))) → p s :=
match s, exists_multiset_eq_map_quot_mk s with
| _, ⟨_t, rfl⟩ => fun h => h _
