English
If the necessary base and coordinate well-foundedness conditions hold, then every x in the DFinsupp space is accessible under Lex provided access is available coordinate-wise.
Русский
При выполнении условий базового основания и координат, любой x в DFinsupp пространстве доступен по 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
instance wellFoundedLT' [∀ i, AddMonoid (α i)] [∀ i, PartialOrder (α i)] [∀ i, CanonicallyOrderedAdd (α i)]
[∀ i, WellFoundedLT (α i)] : WellFoundedLT (Π₀ i, α i) :=
DFinsupp.wellFoundedLT fun _i a => (zero_le a).not_gt
