OAI/Combinatorics/Ryser/Construction/OrdinaryCover.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.ordinaryLines line 12
  2. theorem OAI.RyserCoveringCounterexample.Construction.mem_ordinaryLines line 15
  3. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryVertex_injective line 20
  4. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryLines_card_le line 25
  5. def OAI.RyserCoveringCounterexample.Construction.forcedPencilVertices line 31
  6. theorem OAI.RyserCoveringCounterexample.Construction.card_forcedPencilVertices line 36
  7. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryVertex_mem_forcedPencilVertices_iff line 41
  8. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryLines_offPencil_add_onPencil_le line 55
  9. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryLines_cover_ordinaryPoints line 65
  10. theorem OAI.RyserCoveringCounterexample.Construction.ordinaryVertex_mem_cover_of_pencil_survivors line 77
  11. theorem OAI.RyserCoveringCounterexample.Construction.forcedPencilVertices_subset_cover line 90