English
The order < on ι →₀ ℕ is well-founded.
Русский
Порядок < на ι →₀ ℕ хорошо основан.
LaTeX
$$$$ \mathrm{WellFounded}(<) \text{ on } ι \to_0 \mathbb{N}. $$$$
Lean4
/-- The order on `ι →₀ ℕ` is well-founded. -/
theorem lt_wf : WellFounded (@LT.lt (ι →₀ ℕ) _) :=
Subrelation.wf (sum_id_lt_of_lt _ _) <|
InvImage.wf _
Nat.lt_wfRel.2
-- TODO: generalize to `[WellFoundedRelation α] → WellFoundedRelation (ι →₀ α)`