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)]