restrictTotalDegree_le_restrictDegree

English

restrictTotalDegree σ R m is contained in restrictDegree σ R m.

Русский

restrictTotalDegree σ R m ⊆ restrictDegree σ R m.

LaTeX

$$$\\mathrm{restrictTotalDegree}(\\sigma,R,m) \\leq \\mathrm{restrictDegree}(\\sigma,R,m)$$$

Lean4

theorem restrictTotalDegree_le_restrictDegree (m : ℕ) : restrictTotalDegree σ R m ≤ restrictDegree σ R m := fun p hp ↦
  (mem_restrictDegree _ _ _).mpr fun s hs i ↦
    (degreeOf_le_iff.mp (degreeOf_le_totalDegree p i) s hs).trans ((mem_restrictTotalDegree _ _ _).mp hp)

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