card_interedges_finpartition — Mathlib

English

The total number of interedges between s and t equals the sum over all pairs in s×t of the interedges between f(a) and g(b).

Русский

Общее число ребер между s и t равно сумме по всем парам (a,b) из s×t ребер между f(a) и g(b).

LaTeX

$$$\#(\operatorname{interedges}(r, s, t)) = \#\Bigl((s\times\!\! t)\biUnion (\lambda ab \; , \operatorname{interedges}(r, f(ab.1), g(ab.2)))\Bigr)$$$

Lean4

theorem card_interedges_finpartition [DecidableEq α] [DecidableEq β] (P : Finpartition s) (Q : Finpartition t) :
    #(interedges r s t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2) :=
  by
  rw [card_interedges_finpartition_left _ P, sum_product]
  congr; ext
  rw [card_interedges_finpartition_right]

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