OAI/Combinatorics/SecondNeighborhood/Basic.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SeymourSecondNeighborhood.IsOriented.of_asymmetric line 9
  2. theorem OAI.SeymourSecondNeighborhood.IsOriented.mono line 14
  3. def OAI.SeymourSecondNeighborhood.image line 23
  4. def OAI.SeymourSecondNeighborhood.SecondNeighborhoodConjecture line 27
  5. theorem OAI.SeymourSecondNeighborhood.mem_image line 31
  6. theorem OAI.SeymourSecondNeighborhood.mem_firstNeighbors line 37
  7. theorem OAI.SeymourSecondNeighborhood.mem_secondNeighbors line 42
  8. theorem OAI.SeymourSecondNeighborhood.image_empty line 48
  9. theorem OAI.SeymourSecondNeighborhood.image_singleton line 54
  10. theorem OAI.SeymourSecondNeighborhood.image_mono line 61
  11. theorem OAI.SeymourSecondNeighborhood.image_relation_mono line 68
  12. theorem OAI.SeymourSecondNeighborhood.image_union line 74
  13. theorem OAI.SeymourSecondNeighborhood.image_univ_eq_univ line 92
  14. theorem OAI.SeymourSecondNeighborhood.firstNeighbors_subset_image line 104
  15. theorem OAI.SeymourSecondNeighborhood.self_not_mem_firstNeighbors line 110
  16. theorem OAI.SeymourSecondNeighborhood.self_not_mem_secondNeighbors line 115
  17. theorem OAI.SeymourSecondNeighborhood.first_second_disjoint line 120
  18. theorem OAI.SeymourSecondNeighborhood.no_two_step_self line 127
  19. theorem OAI.SeymourSecondNeighborhood.mem_image_image_singleton line 133
  20. theorem OAI.SeymourSecondNeighborhood.secondNeighbors_eq_image_sdiff line 138
  21. theorem OAI.SeymourSecondNeighborhood.sink_firstNeighbors_eq_empty line 160
  22. theorem OAI.SeymourSecondNeighborhood.sink_secondNeighbors_eq_empty line 166
  23. theorem OAI.SeymourSecondNeighborhood.sink_goodVertex line 174
  24. theorem OAI.SeymourSecondNeighborhood.exists_sink_implies_conjecture line 180