OAI/Combinatorics/BalancedRyser/Probability/ExposureScheduleOrder.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ExposureInterleaving.beforeStrictTotalOrder line 14
  2. abbrev OAI.Balanced.ExposureInterleaving.scheduleLinearOrder line 21
  3. def OAI.Balanced.ExposureInterleaving.schedule line 25
  4. theorem OAI.Balanced.ExposureInterleaving.schedule_lt_iff line 29
  5. theorem OAI.Balanced.ExposureInterleaving.schedule_symm_lt_iff line 36
  6. theorem OAI.Balanced.ExposureInterleaving.schedule_previousD line 41
  7. theorem OAI.Balanced.ExposureInterleaving.schedule_previousC line 49
  8. theorem OAI.Balanced.ExposureInterleaving.previousD_mono_before line 57
  9. theorem OAI.Balanced.ExposureInterleaving.previousC_mono_before line 63
  10. theorem OAI.Balanced.ExposureInterleaving.currentD_mem_previousD line 69
  11. theorem OAI.Balanced.ExposureInterleaving.currentC_mem_previousC line 73
  12. theorem OAI.Balanced.ExposureInterleaving.remainingD_eq_sub_previousD line 77
  13. theorem OAI.Balanced.ExposureInterleaving.remainingC_eq_sub_previousC line 82
  14. theorem OAI.Balanced.ExposureInterleaving.deletion_cutoff_remaining line 87
  15. theorem OAI.Balanced.ExposureInterleaving.previousC_card_le line 96
  16. theorem OAI.Balanced.ExposureInterleaving.schedule_previous_mono line 100
  17. def OAI.Balanced.ExposureInterleaving.schedulePrefix line 106
  18. theorem OAI.Balanced.ExposureInterleaving.mem_schedulePrefix line 109
  19. theorem OAI.Balanced.ExposureInterleaving.schedulePrefix_eq_disjSum line 116
  20. theorem OAI.Balanced.ExposureInterleaving.schedulePrefix_card line 124
  21. theorem OAI.Balanced.ExposureInterleaving.schedule_previous_cards line 130
  22. theorem OAI.Balanced.ExposureInterleaving.schedule_parameter_antitone line 135