OAI/Topology/ArtinGroups/Realizations/RealizeSimplex.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.realizeSimplex line 12
  2. lemma OAI.HarmonicArtin.realizeSimplex_natural line 16
  3. def OAI.HarmonicArtin.prependOrdinal line 27
  4. lemma OAI.HarmonicArtin.prependOrdinal_zero line 42
  5. lemma OAI.HarmonicArtin.prependOrdinal_succ line 44
  6. def OAI.HarmonicArtin.coneSimplex line 48
  7. lemma OAI.HarmonicArtin.coneSimplex_zero line 63
  8. lemma OAI.HarmonicArtin.coneSimplex_one line 68
  9. lemma OAI.HarmonicArtin.map_coneSimplex line 73
  10. def OAI.HarmonicArtin.prependNerve line 88
  11. lemma OAI.HarmonicArtin.prependNerve_natural line 92
  12. lemma OAI.HarmonicArtin.prependNerve_face line 102
  13. def OAI.HarmonicArtin.nerveConeSimplex line 108
  14. lemma OAI.HarmonicArtin.nerveConeSimplex_natural line 112
  15. lemma OAI.HarmonicArtin.nerveConeSimplex_zero line 122
  16. def OAI.HarmonicArtin.nerveBotPoint line 132
  17. lemma OAI.HarmonicArtin.nerveConeSimplex_one line 135
  18. def OAI.HarmonicArtin.nerveConeMap line 148
  19. def OAI.HarmonicArtin.nerveCone line 158
  20. def OAI.HarmonicArtin.pathEvaluate line 161
  21. lemma OAI.HarmonicArtin.nerveCone_zero line 164
  22. lemma OAI.HarmonicArtin.nerveCone_one line 175
  23. theorem OAI.HarmonicArtin.nerve_orderBot_contractible line 186
  24. def OAI.HarmonicArtin.appendOrdinal line 202
  25. lemma OAI.HarmonicArtin.appendOrdinal_last line 219
  26. lemma OAI.HarmonicArtin.appendOrdinal_castSucc line 224
  27. def OAI.HarmonicArtin.topConeSimplex line 231
  28. lemma OAI.HarmonicArtin.topConeSimplex_zero line 247
  29. lemma OAI.HarmonicArtin.topConeSimplex_one line 252
  30. lemma OAI.HarmonicArtin.map_topConeSimplex line 257
  31. def OAI.HarmonicArtin.appendNerve line 271
  32. lemma OAI.HarmonicArtin.appendNerve_natural line 283
  33. lemma OAI.HarmonicArtin.appendNerve_face line 302
  34. def OAI.HarmonicArtin.nerveTopConeSimplex line 310
  35. lemma OAI.HarmonicArtin.nerveTopConeSimplex_natural line 314
  36. lemma OAI.HarmonicArtin.nerveTopConeSimplex_zero line 324
  37. def OAI.HarmonicArtin.nerveTopPoint line 338
  38. lemma OAI.HarmonicArtin.nerveTopConeSimplex_one line 341
  39. def OAI.HarmonicArtin.nerveTopConeMap line 357
  40. def OAI.HarmonicArtin.nerveTopCone line 367
  41. lemma OAI.HarmonicArtin.nerveTopCone_zero line 370
  42. lemma OAI.HarmonicArtin.nerveTopCone_one line 381
  43. theorem OAI.HarmonicArtin.nerve_orderTop_contractible line 392