toNNRat_prod_of_nonneg — Mathlib

English

For a finite s and f: α → ℚ with nonnegativity, the NN Rat embedding preserves products over s: the NN Rat of the product equals the product of the NN Rats.

Русский

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

LaTeX

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

Lean4

theorem toNNRat_prod_of_nonneg {s : Finset α} {f : α → ℚ} (hf : ∀ a ∈ s, 0 ≤ f a) :
    (∏ a ∈ s, f a).toNNRat = ∏ a ∈ s, (f a).toNNRat :=
  by
  rw [← coe_inj, cast_prod, Rat.coe_toNNRat _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs ↦ by rw [Rat.coe_toNNRat _ (hf x hxs)]

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