Caro–Wei theorem

TheoremCaro–Wei bound#✓fully proved

Every finite graph has an independent set of size at least the sum over its vertices of the reciprocal of one more than the degree.

theorem exists_isIndepSet_caroWei :
    ∃ s : Finset V, G.IsIndepSet (s : Set V) ∧
      ∑ v, (1 : ℝ) / (G.degree v + 1) ≤ s.card

Used by 1

Used byCaro–Wei bound for the independence number

TheoremCaro–Wei bound for the independence number#✓fully proved

For every finite simple graph \(G\), the independence number of \(G\) is at least \(\sum_{v} \frac{1}{\deg(v) + 1}\), the sum running over all vertices \(v\) of \(G\).

theorem caroWei_le_indepNum :
    ∑ v, (1 : ℝ) / (G.degree v + 1) ≤ G.indepNum

Uses 1

Proof usesCaro–Wei bound

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.