OAI/Combinatorics/Ryser/Construction/DirectionPlacement.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.directionVector line 10
  2. theorem OAI.RyserCoveringCounterexample.Construction.directionVector_kernel_iff line 14
  3. def OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.directionMap line 20
  4. def OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.projectionScale line 25
  5. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.projectionScale_ne_zero line 30
  6. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.projection_directionMap_apply line 49
  7. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.projection_directionMap_apply_eq_iff line 87
  8. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.directionMap_injective line 96
  9. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.projection_directionMap_placed_eq_iff line 108
  10. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.diagonal_directionMap_none line 120
  11. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.diagonal_directionMap_some line 124
  12. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.extra_directionMap_none line 128
  13. theorem OAI.RyserCoveringCounterexample.Construction.PlaneLinearMap.extra_directionMap_zero line 132
  14. def OAI.RyserCoveringCounterexample.Construction.mapDirection line 142
  15. theorem OAI.RyserCoveringCounterexample.Construction.mapDirection_injective line 144
  16. theorem OAI.RyserCoveringCounterexample.Construction.projection_mapDirection_mapPoint line 156
  17. def OAI.RyserCoveringCounterexample.Construction.placedDirection line 161
  18. theorem OAI.RyserCoveringCounterexample.Construction.placedDirection_injective line 164
  19. theorem OAI.RyserCoveringCounterexample.Construction.projection_placedPoint_eq_iff line 168