OAI/Combinatorics/HadwigerCounterexample/ChannelFrameLaws.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Channel Frame Laws

  1. theorem OAI.HadwigerCounterexample.map_pair_law line 14
  2. theorem OAI.HadwigerCounterexample.mapW_nested line 22
  3. theorem OAI.HadwigerCounterexample.mapW_repeat line 27
  4. theorem OAI.HadwigerCounterexample.mapW_pr_eq line 36
  5. theorem OAI.HadwigerCounterexample.pmax_test line 42
  6. theorem OAI.HadwigerCounterexample.gram_norm_quarter line 61
  7. theorem OAI.HadwigerCounterexample.gramObsCap line 85
  8. abbrev OAI.HadwigerCounterexample.HMat line 129
  9. abbrev OAI.HadwigerCounterexample.HFrame line 130
  10. abbrev OAI.HadwigerCounterexample.HCube line 131
  11. def OAI.HadwigerCounterexample.hchan line 133
  12. def OAI.HadwigerCounterexample.hcube line 135
  13. def OAI.HadwigerCounterexample.lawH line 136
  14. def OAI.HadwigerCounterexample.intoChan line 139
  15. theorem OAI.HadwigerCounterexample.intoChan_inj line 141
  16. theorem OAI.HadwigerCounterexample.intoChan_val line 143
  17. theorem OAI.HadwigerCounterexample.hchan_val line 145
  18. def OAI.HadwigerCounterexample.chanPrice line 150
  19. theorem OAI.HadwigerCounterexample.hchan_cap line 153
  20. theorem OAI.HadwigerCounterexample.hcube_cap line 169