monotone_degree — Mathlib

English

The degree function on DegLex(α →₀ ℕ), given by x ↦ degree(ofDegLex x), is monotone.

Русский

Функция степени на DegLex(α →₀ ℕ), заданная x ↦ deg(ofDegLex x), монотонна.

LaTeX

$$$\text{Monotone}\left( x \mapsto (\operatorname{ofDegLex} x).\operatorname{degree} \right)$$$

Lean4

theorem monotone_degree : Monotone (fun (x : DegLex (α →₀ ℕ)) ↦ (ofDegLex x).degree) :=
  by
  intro x y
  rw [le_iff]
  rintro (h | h)
  · apply le_of_lt h
  · apply le_of_eq h.1

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