English
Generalization of product commutativity when inner finite sets depend on the outer index: if h ensures the right correspondence between (x,y) in s and (x',y') in s' along t and t', then (∀ f) ∏_{x ∈ s} ∏_{y ∈ t(x)} f(x,y) = ∏_{y ∈ t'} ∏_{x ∈ s'(y)} f(x,y).
Русский
Обобщение коммутативности произведений, когда вложенные множества зависят от внешнего индекса: если h обеспечивает соответствие между (x,y) в s и (x',y') в s' вместе с t и t', тогда (для любого f) ∏_{x ∈ s} ∏_{y ∈ t(x)} f(x,y) = ∏_{y ∈ t'} ∏_{x ∈ s'(y)} f(x,y).
LaTeX
$$$$\\forall f:\\ γ \\to α \\to β,\; \\left( \\forall x,y,\\; x \\in s \\land y \\in t(x) \\iff x \\in s'(y) \\land y \\in t'(y) \\right) \\Rightarrow \\prod_{x \\in s} \\prod_{y \\in t(x)} f(x,y) = \\prod_{y \\in t'} \\prod_{x \\in s'(y)} f(x,y). $$$$
Lean4
/-- Generalization of `Finset.prod_comm` to the case when the inner `Finset`s depend on the outer
variable. -/
@[to_additive /-- Generalization of `Finset.sum_comm` to the case when the inner `Finset`s depend on
the outer variable. -/
]
theorem prod_comm' {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ}
(h : ∀ x y, x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} :
(∏ x ∈ s, ∏ y ∈ t x, f x y) = ∏ y ∈ t', ∏ x ∈ s' y, f x y := by
classical
have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1 :=
by
rintro ⟨x, y⟩
simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq, exists_eq_right, ← and_assoc]
exact
(prod_finset_product' _ _ _ this).symm.trans
((prod_finset_product_right' _ _ _) fun ⟨x, y⟩ => (this _).trans ((h x y).trans and_comm))
