sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow

English

Let r be a relation between α and β, and s ⊆ α, t ⊆ β finite. Then the total number of incidences counted by summing the sizes of the bipartite neighborhoods over s equals the total counted by summing the sizes of the corresponding neighborhoods over t. In symbols, ∑_{a∈s} |t.bipartiteAbove r a| = ∑_{b∈t} |s.bipartiteBelow r b|.

Русский

Пусть r — отношение между α и β, s ⊆ α, t ⊆ β — конечно. Тогда сумма размеров окрестностей bipartiteAbove по a из s равна сумме размеров окрестностей bipartiteBelow по b из t: ∑_{a∈s} |t.bipartiteAbove r a| = ∑_{b∈t} |s.bipartiteBelow r b|.

LaTeX

$$$$ \sum_{a \in s} \#(t.bipartiteAbove r a) = \sum_{b \in t} \#(s.bipartiteBelow r b) $$$$

Lean4

theorem sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow [∀ a b, Decidable (r a b)] :
    (∑ a ∈ s, #(t.bipartiteAbove r a)) = ∑ b ∈ t, #(s.bipartiteBelow r b) := by
  simp_rw [card_eq_sum_ones, sum_sum_bipartiteAbove_eq_sum_sum_bipartiteBelow]

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