OAI/Combinatorics/Ryser/Construction/AmbientDeletionGeometry.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.shiftAffineLine line 14
  2. theorem OAI.RyserCoveringCounterexample.Construction.shiftAffineLine_direction line 17
  3. theorem OAI.RyserCoveringCounterexample.Construction.shiftAffineLine_offset line 20
  4. theorem OAI.RyserCoveringCounterexample.Construction.shiftAffineLine_zero line 23
  5. theorem OAI.RyserCoveringCounterexample.Construction.shiftAffineLine_injective line 27
  6. theorem OAI.RyserCoveringCounterexample.Construction.incidence_shiftAffineLine_iff line 37
  7. def OAI.RyserCoveringCounterexample.Construction.ambientLineUnion line 48
  8. theorem OAI.RyserCoveringCounterexample.Construction.mem_ambientLineUnion line 51
  9. theorem OAI.RyserCoveringCounterexample.Construction.mem_ambientLineUnion_shift line 55
  10. theorem OAI.RyserCoveringCounterexample.Construction.card_ambientLineUnion_le line 66
  11. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_ambientLineUnion_shift line 71
  12. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_ambientLineUnion_shift_le line 98
  13. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_image_shiftAffineLine_le line 115
  14. theorem OAI.RyserCoveringCounterexample.Construction.placedPoint_sub_shift line 163
  15. theorem OAI.RyserCoveringCounterexample.Construction.mem_deletedLines_shift line 168
  16. theorem OAI.RyserCoveringCounterexample.Construction.deletedLines_eq_image_shiftAffineLine line 174
  17. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_deletedLines_union line 194
  18. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_deletedLines_union_le line 205
  19. theorem OAI.RyserCoveringCounterexample.Construction.uniform_prob_mem_deletedLines_le line 216