OAI/Combinatorics/Ryser/Construction/DeletionUnionOutside.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.activeDeletionLine line 13
  2. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLine_spec line 18
  3. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLine_mem line 25
  4. theorem OAI.RyserCoveringCounterexample.Construction.incidence_activeDeletionLine line 31
  5. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLine_injective line 37
  6. def OAI.RyserCoveringCounterexample.Construction.activeDeletionLineInPencil line 52
  7. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLineInPencil_surjective line 62
  8. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLineInPencil_bijective line 80
  9. def OAI.RyserCoveringCounterexample.Construction.activeDeletionGroupEquivDeletedPencil line 90
  10. theorem OAI.RyserCoveringCounterexample.Construction.card_deletedPencil_eq_card_activeDeletionGroups line 99
  11. theorem OAI.RyserCoveringCounterexample.Construction.deletedPencil_eq_inter_affinePencil line 107
  12. theorem OAI.RyserCoveringCounterexample.Construction.card_allDeletedLines_inter_affinePencil_eq_card_activeDeletionGroups line 115
  13. theorem OAI.RyserCoveringCounterexample.Construction.activeDeletionLine_many_placedRetainedPoints line 124