English
If w s ≠ 0 and s ∈ support of f, then f(s) ≤ weight w f; otherwise f(s) = 0 and the inequality still holds by nonnegativity.
Русский
Если w(s) ≠ 0 и s принадлежит опоре f, то f(s) ≤ weight w f; иначе f(s)=0 и неравенство по-прежнему выполняется.
LaTeX
$$f s ≤ weight w f$$
Lean4
theorem le_weight (w : σ → ℕ) {s : σ} (hs : w s ≠ 0) (f : σ →₀ ℕ) : f s ≤ weight w f := by
classical
simp only [weight_apply, Finsupp.sum]
by_cases h : s ∈ f.support
· rw [Finset.sum_eq_add_sum_diff_singleton h]
refine le_trans ?_ (Nat.le_add_right _ _)
apply Nat.le_mul_of_pos_right
exact Nat.zero_lt_of_ne_zero hs
· simp only [notMem_support_iff] at h
rw [h]
apply zero_le
