English
Assume r is irreflexive on α. If s is a multiset and every singleton {a} with a ∈ s is accessible under CutExpand r, then s is accessible under CutExpand r.
Русский
Пусть r иррефлексивно на α. Если s — мультимножество и для каждого a ∈ s верно Acc(CutExpand r){a}, то Acc(CutExpand r) s.
LaTeX
$$$ [IsIrrefl \ α \\ r] \Rightarrow (\forall s : Multiset(\alpha), (\forall a \in s, Acc(CutExpand(r))\{a\}) \to Acc(CutExpand(r))\,s) $$$
Lean4
/-- A multiset is accessible under `CutExpand` if all its singleton subsets are,
assuming `r` is irreflexive. -/
theorem acc_of_singleton [IsIrrefl α r] {s : Multiset α} (hs : ∀ a ∈ s, Acc (CutExpand r) { a }) :
Acc (CutExpand r) s := by
induction s using Multiset.induction with
| empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
| cons a s ihs =>
rw [← s.singleton_add a]
rw [forall_mem_cons] at hs
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)
