English
Let r ⊆ γ×α be a finite set, s ⊆ γ, t: γ → Finset α, and h: ∀ p ∈ r, p.1 ∈ s ∧ p.2 ∈ t(p.1). Then for any f: γ×α → β, ∏_{p ∈ r} f(p) = ∏_{c ∈ s} ∏_{a ∈ t(c)} f(c,a).
Русский
Пусть r ⊆ γ×α, s ⊆ γ, t: γ → Finset α, и h: ∀ p ∈ r, p.1 ∈ s ∧ p.2 ∈ t(p.1). Тогда для любого f: γ×α → β выполняется равенство ∏_{p ∈ r} f(p) = ∏_{c ∈ s} ∏_{a ∈ t(c)} f(c,a).
LaTeX
$$$$\\forall f:\\ γ\\times α \\to β,\\; (\\forall p∈r, p.1\\in s ∧ p.2\\in t(p.1)) \\Rightarrow \\prod_{p∈r} f(p) = \\prod_{c∈s} \\prod_{a∈t(c)} f(c,a). $$$$
Lean4
@[to_additive]
theorem prod_finset_product (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α)
(h : ∀ p : γ × α, p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a) :=
by
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.1, p.2))
apply prod_equiv (Equiv.sigmaEquivProd _ _).symm <;> simp [h]
