English
A case principle for strong induction on multisets: to prove a property p for all s, it suffices to prove p(0) and that p(a :: s) follows from p for smaller multisets.
Русский
Принцип разбивки по сильной индукции для мультимножест: чтобы доказать свойство p для всех s, достаточно доказать p(0) и что p(a :: s) следует из p меньших мультимножеств.
LaTeX
$$$p\\;0 \\quad\\text{and}\\quad \\forall a\\ s,\\ (\\forall t \\le s,\\ p(t))\\rightarrow p(a\\;::\\! s) \\Rightarrow p(s)$$$
Lean4
@[elab_as_elim]
theorem case_strongInductionOn {p : Multiset α → Prop} (s : Multiset α) (h₀ : p 0)
(h₁ : ∀ a s, (∀ t ≤ s, p t) → p (a ::ₘ s)) : p s :=
Multiset.strongInductionOn s fun s =>
Multiset.induction_on s (fun _ => h₀) fun _a _s _ ih =>
(h₁ _ _) fun _t h => ih _ <| lt_of_le_of_lt h <| lt_cons_self _ _
