Theorems · Theorem · combinatorics

Rel.card_interedges_finpartition_left

∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α}
  [inst_1 : DecidableEq α] (P : Finpartition s) (t : Finset β),
  (Rel.interedges r s t).card = ∑ a ∈ P.parts, (Rel.interedges r a t).card

Defined in

Mathlib.Combinatorics.SimpleGraph.Density

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidablePredDecidableEq