OAI/Topology/ArtinGroups/Realizations/NerveOrderMap.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.nerveOrderMap line 13
  2. def OAI.HarmonicArtin.nervePrismMap line 16
  3. def OAI.HarmonicArtin.nervePrismReal line 26
  4. def OAI.HarmonicArtin.nervePathEvaluate line 30
  5. lemma OAI.HarmonicArtin.nervePrismReal_zero line 34
  6. lemma OAI.HarmonicArtin.nervePrismReal_one line 49
  7. def OAI.HarmonicArtin.nerveOrderComparisonHomotopy line 64
  8. lemma OAI.HarmonicArtin.nerveOrderMap_id line 73
  9. def OAI.HarmonicArtin.nerveVertex line 82
  10. lemma OAI.HarmonicArtin.simplex_zero_unique line 85
  11. lemma OAI.HarmonicArtin.realizeSimplex_const line 89
  12. lemma OAI.HarmonicArtin.nerveOrderMap_const line 103
  13. theorem OAI.HarmonicArtin.nerve_contractible_of_order_clip line 115