degreeLE_mono — Mathlib

English

If m ≤ n then degreeLE(R,m) is contained in degreeLE(R,n); i.e., the degree bound submodules form a monotone family with respect to the bound.

Русский

Если m ≤ n, то degreeLE(R,m) ⊆ degreeLE(R,n); то есть подмодули с ограничением по степени образуют монотонную семью по пределу степени.

LaTeX

$$$m \le n \implies \operatorname{degreeLE}_R(m) \le \operatorname{degreeLE}_R(n).$$$

Lean4

@[mono]
theorem degreeLE_mono {m n : WithBot ℕ} (H : m ≤ n) : degreeLE R m ≤ degreeLE R n := fun _ hf =>
  mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) H)

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