degree_lt_wf — Mathlib

English

The relation defined by p ≺ q iff deg p < deg q is well-founded on the set of polynomials.

Русский

Отношение, определённое как p ≺ q, если deg p < deg q, является хорошо упорядоченным над множеством многочленов.

LaTeX

$$$\\text{WellFounded}(\\lambda p,q \\in R[X].\\, \\operatorname{degree}(p) < \\operatorname{degree}(q))$$$

Lean4

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

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