prod_range — Mathlib

English

Same as 1964 but with alternative formulations; t.dens equals sum over a in image f of the density of fibers.

Русский

То же самое, что и 1964, но в другой формулировке: dens(t) = ∑_{a ∈ image(f)} dens({b ∈ t | f(b) = a}).

LaTeX

$$$t.dens = \sum_{a \in \mathrm{image}(f)} {b \in t | f(b) = a}.dens$$$

Lean4

@[to_additive]
theorem prod_range [CommMonoid M] {n : ℕ} (f : ℕ → M) : ∏ i ∈ Finset.range n, f i = ∏ i : Fin n, f i :=
  (Fin.prod_univ_eq_prod_range _ _).symm

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