English
A singleton {a} is accessible under CutExpand r if a is accessible under r, assuming r is irreflexive.
Русский
Единичное множество {a} доступно под CutExpand r, если a доступно под r, при условии иррефлексивности r.
LaTeX
$$$ [IsIrrefl \ α \ r] {a} (hacc : Acc r a) : Acc(CutExpand r) \{ a \} $$$
Lean4
/-- A singleton `{a}` is accessible under `CutExpand r` if `a` is accessible under `r`,
assuming `r` is irreflexive. -/
theorem _root_.Acc.cutExpand [IsIrrefl α r] {a : α} (hacc : Acc r a) : Acc (CutExpand r) { a } :=
by
induction hacc with
| _ a h ih
refine Acc.intro _ fun s ↦ ?_
classical
simp only [cutExpand_iff, mem_singleton]
rintro ⟨t, a, hr, rfl, rfl⟩
refine acc_of_singleton fun a' ↦ ?_
rw [erase_singleton, zero_add]
exact ih a' ∘ hr a'
