English
If for every i in the support of x, the index i is accessible and each coordinate i is accessible under Lex, then x is accessible under Lex.
Русский
Если для каждого i из поддержки x i доступен, и каждая координата i доступна по Lex, то и x доступна по Lex.
LaTeX
$$$\\forall x,\\big(\\forall i\\in x.support, Acc(r^c\\cap(\\cdot\\neq\\cdot)) i\\big)\\Rightarrow Acc(DFinsupp.Lex(r,s))\\,x$$$
Lean4
theorem acc (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i)) [DecidableEq ι]
[∀ (i) (x : α i), Decidable (x ≠ 0)] (x : Π₀ i, α i) (h : ∀ i ∈ x.support, Acc (rᶜ ⊓ (· ≠ ·)) i) :
Acc (DFinsupp.Lex r s) x :=
Lex.acc_of_single hbot x fun i hi => Lex.acc_single hbot hs (h i hi) _
