TODO

Rename edgeDensity to edgeDensityBtw

def SimpleGraph.edgeDensity' {α : Type u_1} [Fintype α] (G : SimpleGraph α) [Fintype ↑G.edgeSet] : ℚ≥0

The edge density of a simple graph is its number of edges divided by its number of vertices.

In other words, it is half of its average degree.

Equations

• G.edgeDensity' = ↑G.edgeFinset.card / ↑(Fintype.card α)

noncomputable def SimpleGraph.maxEdgeSubdensity {α : Type u_1} [Fintype α] (G : SimpleGraph α) : ℚ≥0

The maximum edge density of a subgraph of a graph.

Equations

• G.maxEdgeSubdensity = Finset.univ.sup' ⋯ fun (G' : G.Subgraph) => G'.coe.edgeDensity'