English
An induction principle on multisets: if P holds for 0, and if P(s) implies P(insert a s) whenever a ∈ S and s ⊆ S, then P holds for S.
Русский
Принцип индукции по мультимножестам: если P верно для 0, и если P(s) ⇒ P(insert a s) при условиях a ∈ S и s ⊆ S, тогда P верно для S.
LaTeX
$$$\\forall {p:\\mathrm{Multiset} \\alpha \\to \\mathrm{Prop}},\\ (S:\\mathrm{Multiset}\\alpha)\\to p\\,0\\to (\\forall {a s},\\ a \\in S \\to s \\subseteq S \\to p\\,s \\to p\\,(\\mathrm{insert}\\ a\\ s)) \\to p\\,S$$$
Lean4
theorem induction_on' {p : Multiset α → Prop} (S : Multiset α) (h₁ : p 0)
(h₂ : ∀ {a s}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S :=
@Multiset.induction_on α (fun T => T ⊆ S → p T) S (fun _ => h₁)
(fun _ _ hps hs =>
let ⟨hS, sS⟩ := cons_subset.1 hs
h₂ hS sS (hps sS))
(Subset.refl S)
