card_interedges_finpartition_left

English

If P is a finite partition of t, then the number of interedges equals the sum over parts of the interedges inside s and each part.

Русский

Пусть P — конечное разбиение t. Тогда число ребер между s и t равно сумме по частям разбиения числа ребер между s и каждою частью t.

LaTeX

$$$\#(\operatorname{interedges}(r, s, t)) = \sum_{b \in P.part t} \#(\operatorname{interedges}(r, s, b))$$$

Lean4

theorem card_interedges_finpartition_left [DecidableEq α] (P : Finpartition s) (t : Finset β) :
    #(interedges r s t) = ∑ a ∈ P.parts, #(interedges r a t) := by
  classical
  simp_rw [← P.biUnion_parts, interedges_biUnion_left, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

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