prod_fiberwise' — Mathlib

English

A variant of the fiberwise product using the prime form.

Русский

Вариант фиберного произведения с использованием примфорной формы.

LaTeX

$$$\prod_{j\in t} \prod_{i\in s with g(i)=j} f(g(i)) = \prod_{i\in s with g(i)\in t} f(g(i))$$$

Lean4

@[to_additive]
theorem prod_fiberwise' (s : Finset ι) (g : ι → κ) (f : κ → M) : ∏ j, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i) :=
  prod_fiberwise_of_maps_to' (fun _ _ ↦ mem_univ _) _

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