English
Let r be a relation between sets α and β. For finite sets s ⊆ α and t ⊆ β and any function f : α × β → R (where R is a commutative monoid), the incidences counted by first summing over a ∈ s the number of partners b ∈ t with r(a,b), and then taking a product over those partners, equals the incidences counted by summing over b ∈ t the number of partners a ∈ s with r(a,b) and taking the corresponding product. In symbols, ∏_{a∈s} ∏_{b∈t.bipartiteAbove r a} f(a,b) = ∏_{b∈t} ∏_{a∈s.bipartiteBelow r b} f(a,b).
Русский
Пусть r — отношение между множествами α и β. Пусть s ⊆ α и t ⊆ β — конечные множества, и функция f : α × β → R, где R — коммутативное полугруппа. Тогда произведение по a ∈ s и по b ∈ t.bipartiteAbove r a равно произведению по b ∈ t и по a ∈ s.bipartiteBelow r b: ∏_{a∈s} ∏_{b∈t.bipartiteAbove r a} f(a,b) = ∏_{b∈t} ∏_{a∈s.bipartiteBelow r b} f(a,b).
LaTeX
$$$ \displaystyle \prod_{a \in s} \left( \prod_{b \in t\!\cdot\!bipartiteAbove\, r \; a} f(a,b) \right) = \prod_{b \in t} \left( \prod_{a \in s\!\cdot\!bipartiteBelow\, r \; b} f(a,b) \right)$$$
Lean4
@[to_additive]
theorem prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow [CommMonoid R] (f : α → β → R) [∀ a b, Decidable (r a b)] :
∏ a ∈ s, ∏ b ∈ t.bipartiteAbove r a, f a b = ∏ b ∈ t, ∏ a ∈ s.bipartiteBelow r b, f a b :=
by
simp_rw [bipartiteAbove, bipartiteBelow, prod_filter]
exact prod_comm
