coe_prod — Mathlib

English

The Real embedding preserves finite products: (\\\\prod a ∈ s, f a)^\uparrow = \\\\prod a ∈ s, (f a)^\uparrow.

Русский

Преобразование Real сохраняет произведения по конечному множеству: (\\\\prod f a)^\uparrow = \\\\prod (f a)^\uparrow.

LaTeX

$$$\\\\big(\\\\prod a \\\\in s, f a\\\\big)^{\\\\uparrow} = \\\\prod a \\\\in s, (f a)^{\\\\uparrow}.$$$

Lean4

@[simp, norm_cast]
theorem coe_prod (s : Finset ι) (f : ι → ℝ≥0) : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ) :=
  map_prod toRealHom _ _

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