OAI/Combinatorics/SecondNeighborhood/PruningDefinitions.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeymourSecondNeighborhood.Pruning.Conflict line 11
  2. def OAI.SeymourSecondNeighborhood.Pruning.LeftCovers line 14
  3. def OAI.SeymourSecondNeighborhood.Pruning.RightCovers line 17
  4. def OAI.SeymourSecondNeighborhood.Pruning.leftImage line 24
  5. def OAI.SeymourSecondNeighborhood.Pruning.rightImage line 28
  6. def OAI.SeymourSecondNeighborhood.Pruning.Covered line 32
  7. def OAI.SeymourSecondNeighborhood.Pruning.Z line 35
  8. def OAI.SeymourSecondNeighborhood.Pruning.H line 40
  9. def OAI.SeymourSecondNeighborhood.Pruning.ConflictFree line 45
  10. def OAI.SeymourSecondNeighborhood.Pruning.uncoveredZ line 48
  11. structure OAI.SeymourSecondNeighborhood.Pruning.PruningResult line 53
  12. def OAI.SeymourSecondNeighborhood.Pruning.PruningStatement line 62
  13. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_leftImage line 65
  14. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_rightImage line 70
  15. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_Z line 75
  16. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_H line 81
  17. theorem OAI.SeymourSecondNeighborhood.Pruning.mem_uncoveredZ line 87
  18. theorem OAI.SeymourSecondNeighborhood.Pruning.exists_leftCovers_iff line 93
  19. theorem OAI.SeymourSecondNeighborhood.Pruning.exists_rightCovers_iff line 105
  20. theorem OAI.SeymourSecondNeighborhood.Pruning.leftImage_empty line 117
  21. theorem OAI.SeymourSecondNeighborhood.Pruning.rightImage_empty line 122
  22. theorem OAI.SeymourSecondNeighborhood.Pruning.leftImage_mono line 127
  23. theorem OAI.SeymourSecondNeighborhood.Pruning.rightImage_mono line 133
  24. theorem OAI.SeymourSecondNeighborhood.Pruning.Covered.mono line 139
  25. theorem OAI.SeymourSecondNeighborhood.Pruning.Z_eq_inter line 146
  26. theorem OAI.SeymourSecondNeighborhood.Pruning.conflict_corner_mem_Z line 161
  27. theorem OAI.SeymourSecondNeighborhood.Pruning.conflict_corner_mem_H line 166
  28. theorem OAI.SeymourSecondNeighborhood.Pruning.conflictFree_iff_disjoint line 171
  29. theorem OAI.SeymourSecondNeighborhood.Pruning.ConflictFree.mono line 188
  30. theorem OAI.SeymourSecondNeighborhood.Pruning.Z_eq_empty_of_conflictFree line 194
  31. theorem OAI.SeymourSecondNeighborhood.Pruning.H_eq_empty_of_conflictFree line 201
  32. theorem OAI.SeymourSecondNeighborhood.Pruning.conflictFree_left_not_covers_Z line 208
  33. theorem OAI.SeymourSecondNeighborhood.Pruning.conflictFree_right_not_covers_Z line 218
  34. theorem OAI.SeymourSecondNeighborhood.Pruning.uncoveredZ_eq_sdiff line 228
  35. theorem OAI.SeymourSecondNeighborhood.Pruning.pruningResult_self line 234
  36. theorem OAI.SeymourSecondNeighborhood.Pruning.exists_pruning_of_conflictFree line 243