English
If x is a finitely supported function and erasing its value at i is accessible, then the accessibility of the Lex-based structure is inherited by the erased function when the i-th coordinate is removed.
Русский
Если x имеет конечную поддержку и удаление значения на индексе i приводит к доступности, то доступность структуры на основе Lex сохраняется после удаления i-координаты.
LaTeX
$$$\\forall i,\\ Acc(DFinsupp.Lex(r,s))\\big( DFinsupp.single\\ i\\ (x(i))\\big) \\Rightarrow Acc(DFinsupp.Lex(r,s))\\big( DFinsupp.erase\\ i\\ x\\big) \\Rightarrow Acc(DFinsupp.Lex(r,s))\\,x$$$
Lean4
theorem acc_of_single_erase [DecidableEq ι] {x : Π₀ i, α i} (i : ι) (hs : Acc (DFinsupp.Lex r s) <| single i (x i))
(hu : Acc (DFinsupp.Lex r s) <| x.erase i) : Acc (DFinsupp.Lex r s) x := by
classical
convert ← @Acc.of_fibration _ _ _ _ _ (lex_fibration r s) ⟨{ i }, _⟩ (InvImage.accessible snd <| hs.prod_gameAdd hu)
convert piecewise_single_erase x i
