prod_finset_product_right' — Mathlib

English

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

Русский

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

LaTeX

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

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