trailingDegree_lt_wf — Mathlib

English

The relation defined by p ≺ q if trailingDegree(p) < trailingDegree(q) is well-founded on polynomials.

Русский

Отношение p ≺ q, если trailingDegree(p) < trailingDegree(q), является хорошо определённым на полиномах.

LaTeX

$$$\text{WellFounded} \; (\lambda p,q. \operatorname{trailingDegree}(p) < \operatorname{trailingDegree}(q)).$$$

Lean4

theorem trailingDegree_lt_wf : WellFounded fun p q : R[X] => trailingDegree p < trailingDegree q :=
  InvImage.wf trailingDegree wellFounded_lt

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