edgeDensity — Mathlib

English

The edge density between two finite sets is the number of edges between them divided by the product of their sizes.

Русский

Плотность ребер между двумя конечными множествами равна числу ребер между ними, делённому на произведение их размеров.

LaTeX

$$$\operatorname{edgeDensity}(r,s,t) = \dfrac{\#\operatorname{interedges}(r,s,t)}{|s| \cdot |t|}$$$

Lean4

/-- Density of edges of a graph between two finsets of vertices. -/
def edgeDensity : Finset α → Finset α → ℚ :=
  Rel.edgeDensity G.Adj

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