OAI/Combinatorics/HadwigerCounterexample/PolarRankBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Polar Rank Bounds

  1. def OAI.HadwigerCounterexample.swapM line 14
  2. theorem OAI.HadwigerCounterexample.swapM_rank line 17
  3. theorem OAI.HadwigerCounterexample.alt_of_forms line 26
  4. theorem OAI.HadwigerCounterexample.flarge line 38
  5. def OAI.HadwigerCounterexample.urBad line 68
  6. def OAI.HadwigerCounterexample.prodBound line 72
  7. theorem OAI.HadwigerCounterexample.urBad_cap line 74