OAI/Combinatorics/CliqueFree/Peeling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangle_subgraph_surviving_le line 22
2. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangle_deletion_bound line 43
3. def OAI.CliqueFreeIndependence.WeightedGraph.eraseEdge line 69

   Source documentation

   Delete exactly one unordered edge.

   def eraseEdge (G : SimpleGraph V) (u v : V) : SimpleGraph V where
   …

4. lemma OAI.CliqueFreeIndependence.WeightedGraph.eraseEdge_le line 82
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.edgeMass_eraseEdge line 84
6. lemma OAI.CliqueFreeIndependence.WeightedGraph.sum_removed_directed line 108
7. lemma OAI.CliqueFreeIndependence.WeightedGraph.triangleMass_eraseEdge line 128
8. lemma OAI.CliqueFreeIndependence.WeightedGraph.peeling line 135