English
If every coordinate i in the support of x is individually accessible via the Lex order (on single i (x i)), then the whole x is accessible.
Русский
Если для каждого i из поддержки x элемент x i доступен по Lex, то весь x доступен.
LaTeX
$$$\\forall x,\\ (\\forall i\\in x.supp, Acc(DFinsupp.Lex(r,s))\\big( DFinsupp.single\\ i\\ (x(i))\\big)) \\Rightarrow Acc(DFinsupp.Lex(r,s))\\,x$$$
Lean4
theorem acc_of_single (hbot : ∀ ⦃i a⦄, ¬s i a 0) [DecidableEq ι] [∀ (i) (x : α i), Decidable (x ≠ 0)] (x : Π₀ i, α i) :
(∀ i ∈ x.support, Acc (DFinsupp.Lex r s) <| single i (x i)) → Acc (DFinsupp.Lex r s) x :=
by
generalize ht : x.support = t; revert x
classical
induction t using Finset.induction with
| empty =>
intro x ht
rw [support_eq_empty.1 ht]
exact fun _ => Lex.acc_zero hbot
| insert b t hb ih =>
refine fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_
refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_
rw [erase_ne (ha.ne_of_notMem hb)]
exact h a (Finset.mem_insert_of_mem ha)
