OAI/Combinatorics/SecondNeighborhood/ExtremalCompatibility.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeymourSecondNeighborhood.Extremal.Compatible line 13
  2. structure OAI.SeymourSecondNeighborhood.Extremal.Admissible line 16
  3. def OAI.SeymourSecondNeighborhood.Extremal.leftCandidate line 21
  4. def OAI.SeymourSecondNeighborhood.Extremal.rightCandidate line 24
  5. def OAI.SeymourSecondNeighborhood.Extremal.uncovered line 27
  6. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_leftCandidate line 30
  7. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_rightCandidate line 35
  8. theorem OAI.SeymourSecondNeighborhood.Extremal.mem_uncovered line 40
  9. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_compatible line 45
  10. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_admissible line 54
  11. theorem OAI.SeymourSecondNeighborhood.Extremal.column_nonempty_of_diagonal line 60
  12. theorem OAI.SeymourSecondNeighborhood.Extremal.row_nonempty_of_diagonal line 65
  13. theorem OAI.SeymourSecondNeighborhood.Extremal.column_ne_univ_of_compatible line 70
  14. theorem OAI.SeymourSecondNeighborhood.Extremal.row_ne_univ_of_compatible line 82
  15. theorem OAI.SeymourSecondNeighborhood.Extremal.Admissible.strict_leftImage_growth line 94
  16. theorem OAI.SeymourSecondNeighborhood.Extremal.Admissible.strict_rightImage_growth line 102
  17. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_subset_leftCandidate line 110
  18. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_subset_rightCandidate line 124
  19. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_left_conflictFree line 138
  20. theorem OAI.SeymourSecondNeighborhood.Extremal.diagonal_right_conflictFree line 150
  21. theorem OAI.SeymourSecondNeighborhood.Extremal.H_candidates_subset_uncovered line 162
  22. theorem OAI.SeymourSecondNeighborhood.Extremal.H_candidates_card_le_uncovered line 174
  23. theorem OAI.SeymourSecondNeighborhood.Extremal.uncoveredZ_subset_uncovered line 178
  24. theorem OAI.SeymourSecondNeighborhood.Extremal.uncoveredZ_card_le_uncovered line 183
  25. theorem OAI.SeymourSecondNeighborhood.Extremal.pruning_preserves_diagonal line 188