English
Let s be a finite set, t finite, g: ι → κ, f: ι → M. Then the fiberwise product over fibers determined by g and filtered by membership in t equals the fiberwise product where the inner filter uses the preimage under g of t. If the fibers are disjoint, these two products match.
Русский
Пусть s и t конечны, g: ι→κ, f: ι→M. Тогда произведение по волокнам, определённым через g и отфильтрованное по значению t, равно произведению по волокнам, где внутреннее множество фильтруется по предобразу t. При дизъюнктности волокон множества совпадают.
LaTeX
$$$\displaystyle \prod j\in t,\;\prod i\in s\;\text{with } g(i)=j, f(i) = \prod i\in s\;\text{with } g(i)\;\in t, f(i)$$$
Lean4
@[to_additive]
theorem prod_fiberwise_eq_prod_filter (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → M) :
∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i :=
by
rw [← prod_disjiUnion, disjiUnion_filter_eq]
#adaptation_note /-- 2025-09-12 (kmill) copied from private lemma pairwiseDisjoint_fibers -/
intro x' hx y' hy hne
simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl
