Edge density #
This file defines the number and density of edges of a relation/graph.
Main declarations #
Between two finsets of vertices,
Density of a relation #
s₂ ⊆ s₁,
t₂ ⊆ t₁ and they take up all but a
δ-proportion, then the difference in edge
densities is at most
2 * δ.