prod_finset_product' — Mathlib

English

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

Русский

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

LaTeX

$$$$\\prod_{p \\in r} f(p_1, p_2) = \\prod_{c \\in s} \\prod_{a \\in 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.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a :=
  prod_finset_product r s t h

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