OAI/Combinatorics/HadwigerCounterexample/GradientRankBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Gradient Rank Bounds

  1. theorem OAI.HadwigerCounterexample.part_formula_single line 14
  2. theorem OAI.HadwigerCounterexample.shared_at line 37
  3. def OAI.HadwigerCounterexample.routed line 55
  4. theorem OAI.HadwigerCounterexample.role_at line 58
  5. theorem OAI.HadwigerCounterexample.test_rank line 82
  6. def OAI.HadwigerCounterexample.Represents line 87
  7. theorem OAI.HadwigerCounterexample.rep_single line 90
  8. theorem OAI.HadwigerCounterexample.tmix_small line 98
  9. def OAI.HadwigerCounterexample.Xrep line 129
  10. theorem OAI.HadwigerCounterexample.grad_small line 133
  11. theorem OAI.HadwigerCounterexample.Volley.gradient_rep line 221
  12. theorem OAI.HadwigerCounterexample.Volley.here_card line 276
  13. theorem OAI.HadwigerCounterexample.Volley.call_count line 284