sum_le_sum — Mathlib

English

If h1 ≤ h2 pointwise on the support of f, then f.sum h1 ≤ f.sum h2.

Русский

Если для всех i в опоре f выполняется h1 i (f i) ≤ h2 i (f i), то сумма по f для h1 не превосходит сумму по f для h2.

LaTeX

$$$ (\forall i \in f.\mathrm{support}, h_1 i (f i) \le h_2 i (f i)) \Rightarrow f.sum h_1 \le f.sum h_2 $$$

Lean4

@[gcongr]
theorem sum_le_sum (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) : f.sum h₁ ≤ f.sum h₂ :=
  Finset.sum_le_sum h

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