edgeDensity_empty_right — Mathlib

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]

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