Theorems · Definition · combinatorics
SimpleGraph.edgeDensity
{α : Type u_4} → (G : SimpleGraph α) → [DecidableRel G.Adj] → Finset α → Finset α → ℚDensity of edges of a graph between two finsets of vertices.
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableRel
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement and proof · cited by 1,346
- Rel.edgeDensityproof · cited by 12
Cited by35
Results whose statement or proof uses this declaration.
- SimpleGraph.IsUniformproof · cited by 33
- SimpleGraph.regularityReducedproof · cited by 8
- Finpartition.sparsePairsproof · cited by 7
- Finpartition.energyproof · cited by 6
- SimpleGraph.not_isUniform_iffstatement and proof · cited by 5
- SimpleGraph.IsUniform.posproof · cited by 2
- SimpleGraph.edgeDensity_commstatement · cited by 1
- SimpleGraph.edgeDensity_defstatement · cited by 1
- SimpleGraph.edgeDensity_le_onestatement · cited by 1
- SimpleGraph.edgeDensity_nonnegstatement · cited by 1
- SimpleGraph.nonuniformWitnesses_specstatement and proof · cited by 1
- SimpleGraph.isUniform_singletonproof · cited by 1