OAI/Combinatorics/Ryser/LineCover/Deletion.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.LineCover.contribution line 17
  2. def OAI.RyserCoveringCounterexample.LineCover.rare line 20
  3. theorem OAI.RyserCoveringCounterexample.LineCover.contribution_emptyOutcome line 23
  4. theorem OAI.RyserCoveringCounterexample.LineCover.rare_iff_exists line 27
  5. theorem OAI.RyserCoveringCounterexample.LineCover.contribution_card_le line 36
  6. theorem OAI.RyserCoveringCounterexample.LineCover.card_sub_card_le_card_of_sdiff_subset line 51
  7. def OAI.RyserCoveringCounterexample.LineCover.retainedCount line 63
  8. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_update_sdiff_subset line 67
  9. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_sdiff_update_subset line 86
  10. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_update_bounds line 106
  11. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_update_abs_le line 122
  12. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_empty_bounds line 133
  13. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_empty_abs_le line 142
  14. theorem OAI.RyserCoveringCounterexample.LineCover.not_rare_retainedCount_eq line 151
  15. theorem OAI.RyserCoveringCounterexample.LineCover.retainedCount_empty_abs_le_mul line 162
  16. theorem OAI.RyserCoveringCounterexample.LineCover.expectation_card_inter line 176
  17. theorem OAI.RyserCoveringCounterexample.LineCover.prob_nonempty_inter_le line 196
  18. theorem OAI.RyserCoveringCounterexample.LineCover.prob_rare_le line 209
  19. theorem OAI.RyserCoveringCounterexample.LineCover.expectation_retainedCount line 215
  20. theorem OAI.RyserCoveringCounterexample.LineCover.prob_mem_survivors line 221
  21. theorem OAI.RyserCoveringCounterexample.LineCover.expectation_retainedCount_product line 234