OAI/Combinatorics/BalancedRyser/Candidates/CandidateSelectionBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.AvailableCandidate line 15
  2. def OAI.Balanced.actualCandidateGraph line 18
  3. def OAI.Balanced.candidateSelectionInput line 23
  4. theorem OAI.Balanced.subtype_card_of_subset line 30
  5. theorem OAI.Balanced.subtype_inter line 36
  6. theorem OAI.Balanced.candidateSelection_slot_eq line 43
  7. theorem OAI.Balanced.candidateSelection_neighbors_eq line 51
  8. theorem OAI.Balanced.candidateSelection_slot_card line 60
  9. theorem OAI.Balanced.candidateSelection_neighbors_card line 67
  10. theorem OAI.Balanced.candidateSelection_neighbor_slot_card line 74
  11. theorem OAI.Balanced.candidateSelection_common_neighbors_card line 84
  12. theorem OAI.Balanced.candidateGraphGood_selection line 94
  13. theorem OAI.Balanced.candidateSelection_lineAssignment line 142
  14. theorem OAI.Balanced.candidateSelection_selector_of_transversal line 155
  15. theorem OAI.Balanced.candidateSelection_configuration_of_transversal line 174