OAI/Combinatorics/HadwigerCounterexample/CoverSpaces.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cover Spaces

  1. def OAI.HadwigerCounterexample.prj line 14
  2. theorem OAI.HadwigerCounterexample.prj_data line 17
  3. def OAI.HadwigerCounterexample.chop line 21
  4. theorem OAI.HadwigerCounterexample.chop_ker line 23
  5. theorem OAI.HadwigerCounterexample.chop_colT line 30
  6. theorem OAI.HadwigerCounterexample.vanish_chop line 41
  7. def OAI.HadwigerCounterexample.chopSpace line 61
  8. theorem OAI.HadwigerCounterexample.chopSpace_join line 63
  9. theorem OAI.HadwigerCounterexample.chopSpace_disjoint line 77
  10. theorem OAI.HadwigerCounterexample.chopSpace_rank line 85
  11. abbrev OAI.HadwigerCounterexample.Cov line 91
  12. def OAI.HadwigerCounterexample.cdSign line 92
  13. def OAI.HadwigerCounterexample.cdim line 94
  14. theorem OAI.HadwigerCounterexample.cdim_sign line 95
  15. def OAI.HadwigerCounterexample.epoch line 99
  16. def OAI.HadwigerCounterexample.matter line 101
  17. theorem OAI.HadwigerCounterexample.matter_dim line 104
  18. def OAI.HadwigerCounterexample.erased line 107
  19. def OAI.HadwigerCounterexample.covered line 110
  20. theorem OAI.HadwigerCounterexample.covered_iff line 113
  21. theorem OAI.HadwigerCounterexample.covered_part line 122
  22. def OAI.HadwigerCounterexample.coverX line 130

    Source documentation

    Cover as a tensor space; used to count tiny-cover span.

    def coverX (p : Shape) {N} (S : Cov p N) := ker (erased p S)

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Cov, OAI.HadwigerCounterexample.erased

  23. theorem OAI.HadwigerCounterexample.vanish_sum line 132
  24. theorem OAI.HadwigerCounterexample.cover_mem line 167
  25. theorem OAI.HadwigerCounterexample.cov_pi_bound line 171
  26. theorem OAI.HadwigerCounterexample.cover_dim line 185