toNNRat_sum_of_nonneg — Mathlib

English

For a finite s and f: α → ℚ with f(a) ≥ 0 for a ∈ s, the nonnegative-ratio embedding commutes with finite sums: the NN Rat of the sum equals the sum of the NN Rat of the terms.

Русский

Пусть s конечно, f: α → ℚ и для всех a ∈ s выполнено f(a) ≥ 0. Приведение в NN Rat сохраняет суммы: NN Rat от суммы равен сумме NN Rat от слагаемых.

LaTeX

$$$\left(\sum_{a \in s} f(a)\right).toNNRat = \sum_{a \in s} (f(a)).toNNRat$$$

Lean4

theorem toNNRat_sum_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a, a ∈ s → 0 ≤ f a) :
    (∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat :=
  by
  rw [← coe_inj, cast_sum, Rat.coe_toNNRat _ (Finset.sum_nonneg hf)]
  exact Finset.sum_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

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