lt_wf — Mathlib

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 (ι →₀ α)`

Похожие утверждения