OAI/Combinatorics/CliqueFree/Projection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CliqueFreeIndependence.WeightedGraph.sum_injective_le line 22
2. structure OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection line 31

   Source documentation

   A weight-preserving, directed-edge-injective projection.

   structure EdgeProjection (H : SimpleGraph U) (G : SimpleGraph V) (π : U → V) : Prop where
   …

3. def OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.edgeMap line 38
4. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.edgeMap_injective line 42
5. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.mass_image_le line 50
6. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.crossMass_edge_sum line 55
7. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.crossMass_le line 73
8. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.crossBound line 97
9. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.edgeMass_le line 106
10. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.neighbor_injective line 119
11. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.neighborhood_image line 124
12. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeProjection.neighborMass_le line 130