le_degree — Mathlib

English

For every s ∈ σ, the coefficient f(s) is at most deg f: f(s) ≤ deg f.

Русский

Для каждого s ∈ σ коэффициент f(s) не превосходит deg f: f(s) ≤ deg f.

LaTeX

$$$f(s) \le \deg f$$$

Lean4

theorem le_degree {R : Type*} [AddCommMonoid R] [PartialOrder R] [CanonicallyOrderedAdd R] (s : σ) (f : σ →₀ R) :
    f s ≤ degree f := by
  by_cases h : s ∈ f.support
  · exact Finset.single_le_sum_of_canonicallyOrdered h
  · simp only [notMem_support_iff] at h
    simp only [h, zero_le]

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