card_interedges_finpartition_right

English

A shorthand for the right-partition edge count equality.

Русский

Кратко о подсчете ребер справа в разбиении.

LaTeX

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

Lean4

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

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