OAI/Combinatorics/Ryser/Incidence/ScalarCoverExpressions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.RyserCoveringCounterexample.Incidence.ScalarExpression line 14
  2. def OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent line 32
  3. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_zero line 36
  4. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_succ line 39
  5. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_le_succ line 43
  6. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_monotone line 48
  7. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_ge_four line 52
  8. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_twice_add line 56
  9. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_closed_form line 64
  10. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_inv_bound line 69
  11. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_add_bound line 74
  12. theorem OAI.RyserCoveringCounterexample.Incidence.scalarCoverExponent_mul_bound line 84
  13. theorem OAI.RyserCoveringCounterexample.Incidence.ScalarExpression.scalarCovered line 96
  14. theorem OAI.RyserCoveringCounterexample.Incidence.ScalarExpression.scalarCovered_of_le line 127
  15. theorem OAI.RyserCoveringCounterexample.Incidence.ScalarExpression.card_add_of_le line 139
  16. theorem OAI.RyserCoveringCounterexample.Incidence.ScalarExpression.card_add_subset_of_le line 151
  17. theorem OAI.RyserCoveringCounterexample.Incidence.scalarExpression_ratio line 170