OAI/Combinatorics/Ryser/Construction/GroupSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.groupSelectionData line 14
  2. theorem OAI.RyserCoveringCounterexample.Construction.groupSelectionData_W_equivFin line 19
  3. theorem OAI.RyserCoveringCounterexample.Construction.groupSelectionData_dirs_equivFin line 25
  4. def OAI.RyserCoveringCounterexample.Construction.groupSelectionConstant line 31
  5. theorem OAI.RyserCoveringCounterexample.Construction.card_groups_le_two_mul_card line 33
  6. theorem OAI.RyserCoveringCounterexample.Construction.groupSelectionData_direction_multiplicity_le_two line 43
  7. theorem OAI.RyserCoveringCounterexample.Construction.groupSelectionData_bounded line 58
  8. def OAI.RyserCoveringCounterexample.Construction.selectedShifts line 85
  9. theorem OAI.RyserCoveringCounterexample.Construction.selectedShifts_projection_ne line 92
  10. theorem OAI.RyserCoveringCounterexample.Construction.selectedShifts_deletionSeparated line 127
  11. theorem OAI.RyserCoveringCounterexample.Construction.exists_selectedShifts_deletionSeparated line 145