OAI/Combinatorics/SecondNeighborhood/AugmentedGraph.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeymourSecondNeighborhood.Pruning.LeftVertex line 13
  2. abbrev OAI.SeymourSecondNeighborhood.Pruning.RightVertex line 16
  3. def OAI.SeymourSecondNeighborhood.Pruning.AugmentedEdge line 19
  4. def OAI.SeymourSecondNeighborhood.Pruning.OriginalRelation line 26
  5. def OAI.SeymourSecondNeighborhood.Pruning.AlphaRelation line 29
  6. def OAI.SeymourSecondNeighborhood.Pruning.BetaRelation line 32
  7. def OAI.SeymourSecondNeighborhood.Pruning.originalLift line 37
  8. def OAI.SeymourSecondNeighborhood.Pruning.alphaLift line 40
  9. def OAI.SeymourSecondNeighborhood.Pruning.betaLift line 44
  10. theorem OAI.SeymourSecondNeighborhood.Pruning.originalLift_injective line 48
  11. theorem OAI.SeymourSecondNeighborhood.Pruning.alphaLift_injective line 54
  12. theorem OAI.SeymourSecondNeighborhood.Pruning.betaLift_injective line 60
  13. def OAI.SeymourSecondNeighborhood.Pruning.originalEdges line 66
  14. def OAI.SeymourSecondNeighborhood.Pruning.alphaEdges line 71
  15. def OAI.SeymourSecondNeighborhood.Pruning.betaEdges line 77
  16. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_originalEdges line 83
  17. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_alphaEdges line 89
  18. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_betaEdges line 95
  19. theorem OAI.SeymourSecondNeighborhood.Pruning.originalEdges_isMatching line 101
  20. theorem OAI.SeymourSecondNeighborhood.Pruning.alphaEdges_isMatching line 117
  21. theorem OAI.SeymourSecondNeighborhood.Pruning.betaEdges_isMatching line 133
  22. theorem OAI.SeymourSecondNeighborhood.Pruning.original_alpha_left_ne line 149
  23. theorem OAI.SeymourSecondNeighborhood.Pruning.original_beta_right_ne line 160
  24. theorem OAI.SeymourSecondNeighborhood.Pruning.alphaEdges_image line 171
  25. theorem OAI.SeymourSecondNeighborhood.Pruning.betaEdges_image line 194
  26. theorem OAI.SeymourSecondNeighborhood.Pruning.augmented_matching_eq_three_images line 214
  27. theorem OAI.SeymourSecondNeighborhood.Pruning.augmented_matching_card line 249