le_weight_of_ne_zero — Mathlib

English

If w s ≠ 0 then f s ≤ weight w f for all f in σ →₀ ℕ; in particular, if f s ≠ 0 then w s ≤ weight w f.

Русский

Если w(s) ≠ 0, то для любых f ∈ σ →₀ ℕ верно f(s) ≤ weight w f; в частности, если f(s) ≠ 0, то w(s) ≤ weight w f.

LaTeX

$$f s ≤ weight w f$$

Lean4

theorem le_weight_of_ne_zero (hw : ∀ s, 0 ≤ w s) {s : σ} {f : σ →₀ ℕ} (hs : f s ≠ 0) : w s ≤ weight w f := by
  classical
  simp only [weight_apply, Finsupp.sum]
  trans f s • w s
  · apply le_smul_of_one_le_left (hw s)
    exact Nat.one_le_iff_ne_zero.mpr hs
  · rw [← Finsupp.mem_support_iff] at hs
    rw [Finset.sum_eq_add_sum_diff_singleton hs]
    exact le_add_of_nonneg_right <| Finset.sum_nonneg <| fun i _ ↦ nsmul_nonneg (hw i) (f i)

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