English
If the index i evolves independently under a base relation, then the dependent function concentrated at i is well-founded with respect to the Lex order.
Русский
Если i эволюционирует независимо относительно базового отношения, то функция, сосредоточенная в i, хорошо упорядочена по Lex.
LaTeX
$$$\\forall i,\\ Acc(r^c\\cap(\\cdot\\neq\\cdot))(i)\\Rightarrow\\forall a,\\ Acc(DFinsupp.Lex(r,s))\\ big( DFinsupp.single\\ i\\ a \\big)$$$
Lean4
theorem acc_single (hbot : ∀ ⦃i a⦄, ¬s i a 0) (hs : ∀ i, WellFounded (s i)) [DecidableEq ι] {i : ι}
(hi : Acc (rᶜ ⊓ (· ≠ ·)) i) : ∀ a, Acc (DFinsupp.Lex r s) (single i a) :=
by
induction hi with
| _ i _ ih
refine fun a => WellFounded.induction (hs i) (C := fun x ↦ Acc (DFinsupp.Lex r s) (single i x)) a fun a ha ↦ ?_
refine Acc.intro _ fun x ↦ ?_
rintro ⟨k, hr, hs⟩
rw [single_apply] at hs
split_ifs at hs with hik
swap
· exact (hbot hs).elim
subst hik
classical
refine Lex.acc_of_single hbot x fun j hj ↦ ?_
obtain rfl | hij := eq_or_ne j i
· exact ha _ hs
by_cases h : r j i
· rw [hr j h, single_eq_of_ne hij, single_zero]
exact Lex.acc_zero hbot
· exact ih _ ⟨h, hij⟩ _
