OAI/Combinatorics/Ryser/LineCover/DeletionDefinitions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RyserCoveringCounterexample.LineCover.Outcome line 13
  2. def OAI.RyserCoveringCounterexample.LineCover.emptyOutcome line 16
  3. def OAI.RyserCoveringCounterexample.LineCover.deleted line 21
  4. theorem OAI.RyserCoveringCounterexample.LineCover.mem_deleted line 24
  5. theorem OAI.RyserCoveringCounterexample.LineCover.deleted_emptyOutcome line 29
  6. def OAI.RyserCoveringCounterexample.LineCover.selected line 33
  7. theorem OAI.RyserCoveringCounterexample.LineCover.mem_selected line 36
  8. def OAI.RyserCoveringCounterexample.LineCover.survivors line 42
  9. theorem OAI.RyserCoveringCounterexample.LineCover.mem_survivors line 46
  10. theorem OAI.RyserCoveringCounterexample.LineCover.mem_survivors_active line 51
  11. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_mono_ignore line 65
  12. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_insert_eq_of_not_selected line 75
  13. theorem OAI.RyserCoveringCounterexample.LineCover.selected_of_survivors_insert_ne line 83
  14. theorem OAI.RyserCoveringCounterexample.LineCover.not_ignored_of_survivors_insert_ne line 90
  15. def OAI.RyserCoveringCounterexample.LineCover.cleanCover line 97
  16. theorem OAI.RyserCoveringCounterexample.LineCover.survivors_inter_cleanCover line 101
  17. theorem OAI.RyserCoveringCounterexample.LineCover.cleanCover_covers line 122
  18. theorem OAI.RyserCoveringCounterexample.LineCover.cleanCover_card_le line 131