instWellFoundedRelationWithTopNat

English

The relation < on WithTop(ℕ) is a well-founded order: every nonempty subset of WithTop(ℕ) has a minimal element with respect to <.

Русский

Отношение < на WithTop(ℕ) образует хорошо основанный порядок: любая непустая подмножество WithTop(ℕ) имеет минимальный элемент по отношению к <.

LaTeX

$$$\mathrm{WellFounded}((\mathrm{WithTop}\,\mathbb{N}, <))$$$

Lean4

instance : WellFoundedRelation (WithTop ℕ) where
  rel := (· < ·)
  wf := IsWellFounded.wf

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