prod_finset_product_right — Mathlib

English

Let r ⊆ α×γ, s ⊆ γ, t: γ → Finset α, and f: α×γ → β. Then ∏_{p ∈ r} f(p) = ∏_{c ⊆ s} ∏_{a ∈ t(c)} f(a,c).

Русский

Пусть r ⊆ α×γ, s ⊆ γ, t: γ → Finset α, и f: α×γ → β. Тогда ∏_{p ∈ r} f(p) = ∏_{c ∈ s} ∏_{a ∈ t(c)} f(a,c).

LaTeX

$$$$\\prod_{p \\in r} f(p) = \\prod_{c \\in s} \\prod_{a \\in t(c)} f(a,c). $$$$

Lean4

@[to_additive]
theorem prod_finset_product_right (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α)
    (h : ∀ p : α × γ, p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c) :=
  by
  refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))
  apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]

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