OAI/Combinatorics/Ryser/Selection/Definitions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RyserCoveringCounterexample.Selection.Data line 12
  2. abbrev OAI.RyserCoveringCounterexample.Selection.Position line 16
  3. abbrev OAI.RyserCoveringCounterexample.Selection.Pool line 17
  4. def OAI.RyserCoveringCounterexample.Selection.Conflict line 21
  5. theorem OAI.RyserCoveringCounterexample.Selection.projection_sub_eq line 25
  6. theorem OAI.RyserCoveringCounterexample.Selection.projection_add_eq line 29
  7. theorem OAI.RyserCoveringCounterexample.Selection.conflict_iff_forbidden line 33
  8. theorem OAI.RyserCoveringCounterexample.Selection.Conflict.symm line 50
  9. theorem OAI.RyserCoveringCounterexample.Selection.conflict_comm line 58
  10. def OAI.RyserCoveringCounterexample.Selection.HasCompatibleChoice line 62
  11. def OAI.RyserCoveringCounterexample.Selection.Feasible line 66
  12. theorem OAI.RyserCoveringCounterexample.Selection.feasible_empty line 70
  13. theorem OAI.RyserCoveringCounterexample.Selection.feasible_mono line 74
  14. theorem OAI.RyserCoveringCounterexample.Selection.feasible_congr line 79
  15. def OAI.RyserCoveringCounterexample.Selection.Bounded line 91
  16. def OAI.RyserCoveringCounterexample.Selection.feasibleSet line 97
  17. theorem OAI.RyserCoveringCounterexample.Selection.mem_feasibleSet line 102
  18. theorem OAI.RyserCoveringCounterexample.Selection.feasibleSet_empty line 108
  19. theorem OAI.RyserCoveringCounterexample.Selection.feasibleSet_mono line 114
  20. def OAI.RyserCoveringCounterexample.Selection.feasibleMass line 121
  21. def OAI.RyserCoveringCounterexample.Selection.exposedCount line 125