English
If P is a finite partition of s, then the number of interedges equals the sum over parts of the interedges inside each part to t.
Русский
Пусть P — конечное разбиение s. Тогда число ребер между s и t равно сумме по частям разбиения числа ребер между каждою частью и t.
LaTeX
$$$\#(\operatorname{interedges}(r, s, t)) = \sum_{a \in P.part s} \#(\operatorname{interedges}(r, a, t))$$$
Lean4
@[simp]
theorem edgeDensity_empty_right (s : Finset α) : edgeDensity r s ∅ = 0 := by
rw [edgeDensity, Finset.card_empty, Nat.cast_zero, mul_zero, div_zero]