instIsWellFoundedInvImageNatLt — Mathlib

English

If f : α → ℕ, then the inverse-image of the usual natual-number order under f is well-founded on α.

Русский

Если $f:\\alpha\\to\\mathbb{N}$, то обратное изображение обычного порядка на $\mathbb{N}$ под действием $f$ на $\alpha$ является хорошо основанным.

LaTeX

$$IsWellFounded(α, InvImage(\\lt, f))$$

Lean4

instance (f : α → ℕ) : IsWellFounded _ (InvImage (· < ·) f) :=
  ⟨(measure f).wf⟩

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