English
Let s and t be multisets with s ≤ t. If a binary predicate C on pairs of multisets holds for every pair of lists l1, l2 where l1 is a sublist of l2 (in the sense of list substructure), then C holds for the pair (s, t).
Русский
Пусть s и t — мультисеты такие, что s ≤ t. Если для любой пары списков l1, l2, где l1 является подпоследовательностью l2, свойство C выполняется для соответствующих мультисетов ⟦l1⟧ и ⟦l2⟧, то C выполняется и для пары (s, t).
LaTeX
$$$\\forall \\alpha\\,\\forall C:(\\mathcal{M}(\\alpha)\\times\\mathcal{M}(\\alpha)\\to\\mathrm{Prop}),\\\\forall s,t\\in\\mathcal{M}(\\alpha),\\ s\\le t\\to\\Big(\\forall l_1,l_2\\in\\mathrm{List}(\\alpha),\\ l_1<+l_2\\to C(\\operatorname{ofList}l_1,\\operatorname{ofList}l_2)\\Big)\\to C(s,t).$$$
Lean4
@[elab_as_elim]
theorem leInductionOn {C : Multiset α → Multiset α → Prop} {s t : Multiset α} (h : s ≤ t)
(H : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → C l₁ l₂) : C s t :=
Quotient.inductionOn₂ s t (fun l₁ _ ⟨l, p, s⟩ => (show ⟦l⟧ = ⟦l₁⟧ from Quot.sound p) ▸ H s) h
