OAI/Combinatorics/Ryser/Construction/CosetDirections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.cosetPlacement line 13
  2. theorem OAI.RyserCoveringCounterexample.Construction.placedDirection_coset_none line 17
  3. theorem OAI.RyserCoveringCounterexample.Construction.placedDirection_coset_some line 21
  4. theorem OAI.RyserCoveringCounterexample.Construction.coset_axisDirections line 27
  5. theorem OAI.RyserCoveringCounterexample.Construction.mem_coset_altered_iff line 32
  6. theorem OAI.RyserCoveringCounterexample.Construction.none_notMem_coset_altered line 39
  7. theorem OAI.RyserCoveringCounterexample.Construction.zero_notMem_coset_altered line 43
  8. theorem OAI.RyserCoveringCounterexample.Construction.unitCoset_mul_embedded line 51
  9. theorem OAI.RyserCoveringCounterexample.Construction.some_unit_mem_coset_altered_iff line 57
  10. theorem OAI.RyserCoveringCounterexample.Construction.existsUnique_coset_altered line 76
  11. theorem OAI.RyserCoveringCounterexample.Construction.coset_altered_index_eq line 83
  12. theorem OAI.RyserCoveringCounterexample.Construction.disjoint_coset_altered line 96
  13. theorem OAI.RyserCoveringCounterexample.Construction.identity_coset_altered line 104