instWellFoundedRelationNat — Mathlib

English

There exists a well-founded relation on ι →₀ ℕ given by the usual less-than relation.

Русский

Существует хорошо основанное отношение на ι →₀ ℕ, заданное обычным отношением «меньше».

LaTeX

$$$$ \text{There exists a WellFoundedRelation}(ι \to_0 \mathbb{N}) \text{ with } \mathrm{rel} = <. $$$$

Lean4

instance : WellFoundedRelation (ι →₀ ℕ) where
  rel := (· < ·)
  wf := lt_wf _

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