card_interedges_div_card — Mathlib

English

Let s and t be finite subsets of the vertex set. The density of edges between s and t is exactly the number of interedges between s and t, divided by the product |s| · |t|.

Русский

Пусть s и t — конечные подмножества множества вершин. Плотность рёбер между s и t равна количеством межрёбер между s и t, делённому на произведение |s|·|t|.

LaTeX

$$$\frac{\#(G.interedges s t)}{\#s \cdot \#t} = G.edgeDensity s t$$$

Lean4

theorem card_interedges_div_card (s t : Finset α) : (#(G.interedges s t) : ℚ) / (#s * #t) = G.edgeDensity s t :=
  rfl

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