OAI/Combinatorics/SecondNeighborhood/Matching.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeymourSecondNeighborhood.Bipartite.IsMatching line 12
  2. def OAI.SeymourSecondNeighborhood.Bipartite.IsMaximumMatching line 17
  3. def OAI.SeymourSecondNeighborhood.Bipartite.IsVertexCover line 20
  4. theorem OAI.SeymourSecondNeighborhood.Bipartite.isMatching_empty line 23
  5. theorem OAI.SeymourSecondNeighborhood.Bipartite.IsMatching.submatching line 27
  6. theorem OAI.SeymourSecondNeighborhood.Bipartite.IsMatching.mono_relation line 35
  7. theorem OAI.SeymourSecondNeighborhood.Bipartite.IsMatching.left_unique line 39
  8. theorem OAI.SeymourSecondNeighborhood.Bipartite.IsMatching.right_unique line 44
  9. def OAI.SeymourSecondNeighborhood.Bipartite.leftVertices line 53
  10. def OAI.SeymourSecondNeighborhood.Bipartite.rightVertices line 55
  11. theorem OAI.SeymourSecondNeighborhood.Bipartite.mem_leftVertices line 58
  12. theorem OAI.SeymourSecondNeighborhood.Bipartite.mem_rightVertices line 69
  13. theorem OAI.SeymourSecondNeighborhood.Bipartite.matching_card_leftVertices line 80
  14. theorem OAI.SeymourSecondNeighborhood.Bipartite.matching_card_rightVertices line 85
  15. theorem OAI.SeymourSecondNeighborhood.Bipartite.matching_card_le_cover_card line 90
  16. theorem OAI.SeymourSecondNeighborhood.Bipartite.exists_maximum_matching line 121
  17. theorem OAI.SeymourSecondNeighborhood.Bipartite.exists_maximum_matching_min_cost line 133