OAI/Combinatorics/Ryser/Incidence/RatioSet.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Incidence.ratioSet line 13
  2. def OAI.RyserCoveringCounterexample.Incidence.dilateSum line 16
  3. theorem OAI.RyserCoveringCounterexample.Incidence.mem_dilateSum line 19
  4. theorem OAI.RyserCoveringCounterexample.Incidence.mem_ratioSet line 29
  5. theorem OAI.RyserCoveringCounterexample.Incidence.mem_ratioSet_of_collision line 47
  6. theorem OAI.RyserCoveringCounterexample.Incidence.mem_ratioSet_of_dilateSum_card_lt line 66
  7. theorem OAI.RyserCoveringCounterexample.Incidence.zero_mem_ratioSet line 80
  8. theorem OAI.RyserCoveringCounterexample.Incidence.one_mem_ratioSet line 85
  9. theorem OAI.RyserCoveringCounterexample.Incidence.neg_mem_ratioSet line 91
  10. theorem OAI.RyserCoveringCounterexample.Incidence.inv_mem_ratioSet line 98
  11. def OAI.RyserCoveringCounterexample.Incidence.ratioSubfield line 110
  12. theorem OAI.RyserCoveringCounterexample.Incidence.mem_ratioSubfield line 123
  13. theorem OAI.RyserCoveringCounterexample.Incidence.card_le_card_ratioSet line 130