OAI/Combinatorics/CliqueFree/EdgeState.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CliqueFreeIndependence.WeightedGraph.EdgeState line 20

    Source documentation

    Oriented edges, the disjoint union of the neighborhood state spaces.

    abbrev EdgeState (G : SimpleGraph V) := {e : V × V // G.Adj e.1 e.2}
  2. instance OAI.CliqueFreeIndependence.WeightedGraph.edgeStateFintype line 22
  3. def OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.src line 30
  4. def OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.dst line 31
  5. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.adj line 33
  6. def OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.rev line 35
  7. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.src_rev line 37
  8. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.dst_rev line 39
  9. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.rev_rev line 41
  10. def OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.revEquiv line 43
  11. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.sum_eq line 49
  12. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.sum_fiber line 57
  13. lemma OAI.CliqueFreeIndependence.WeightedGraph.EdgeState.sum_fiber' line 63
  14. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_nonneg line 70
  15. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_zero line 73
  16. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_small line 75
  17. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_large line 80
  18. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_mono line 84
  19. lemma OAI.CliqueFreeIndependence.WeightedGraph.growth_le_twice line 110
  20. lemma OAI.CliqueFreeIndependence.WeightedGraph.mass_union_le line 130