OAI/Combinatorics/Ryser/Construction/AmbientDeletionShapes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.ambientShapes line 19
  2. theorem OAI.RyserCoveringCounterexample.Construction.linePoints_mem_ambientShapes line 22
  3. theorem OAI.RyserCoveringCounterexample.Construction.ambient_linePoints_injective line 25
  4. theorem OAI.RyserCoveringCounterexample.Construction.ambientShapes_count_le line 32
  5. theorem OAI.RyserCoveringCounterexample.Construction.ambientShapes_size_le line 44
  6. theorem OAI.RyserCoveringCounterexample.Construction.ambientShapes_sparse line 51
  7. def OAI.RyserCoveringCounterexample.Construction.ambientLineOutcome line 58
  8. theorem OAI.RyserCoveringCounterexample.Construction.mem_deleted_ambientLineOutcome line 63
  9. theorem OAI.RyserCoveringCounterexample.Construction.ambientLineOutcome_lists_line line 76
  10. theorem OAI.RyserCoveringCounterexample.Construction.deleted_empty_ambientLineOutcome line 87
  11. def OAI.RyserCoveringCounterexample.Construction.ambientDeletionConstant line 94
  12. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionConstant_two_le line 97
  13. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionConstant_lines_le line 102
  14. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionConstant_trials_le line 107
  15. theorem OAI.RyserCoveringCounterexample.Construction.ambientDeletionConstant_lineRate_le line 112