tsum_mono_subtype — Mathlib

English

If s ⊆ t are sets of indices and f is the same function, then the sum over s-subtype is ≤ the sum over t-subtype.

Русский

Если s ⊆ t, то сумма по подтипу s меньше или равна сумме по подтипу t.

LaTeX

$$$\sum' x : s, f(x) \le \sum' x : t, f(x),$ где s ⊆ t.$$

Lean4

theorem tsum_mono_subtype (f : α → ℝ≥0∞) {s t : Set α} (h : s ⊆ t) : ∑' x : s, f x ≤ ∑' x : t, f x :=
  tsum_comp_le_tsum_of_injective (inclusion_injective h) _

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