English
An accessibility (Acc) result for Finsupp.Lex: under suitable hbot, hs, hr, any x ∈ Finsupp α N is Acc under Finsupp.Lex r s.
Русский
Равенство доступности (Acc) для Finsupp.Lex: при разумных условиях hbot, hs, hr любой x ∈ Finsupp α N удовлетворяет Acc по Finsupp.Lex r s.
LaTeX
$$$\forall x : \sigma \to_0 N, AcC (Finsupp.Lex r s) x$$$
Lean4
/-- Transferred from `DFinsupp.Lex.acc`. See the top of that file for an explanation for the
appearance of the relation `rᶜ ⊓ (≠)`. -/
theorem acc (hbot : ∀ ⦃n⦄, ¬s n 0) (hs : WellFounded s) (x : α →₀ N) (h : ∀ a ∈ x.support, Acc (rᶜ ⊓ (· ≠ ·)) a) :
Acc (Finsupp.Lex r s) x := by
rw [lex_eq_invImage_dfinsupp_lex]
classical
refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)
simpa only [toDFinsupp_support] using h
