OAI/GroupTheory/FiniteType/DuffySimplex.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DuffySimplex.Std line 22
  2. def OAI.DuffySimplex.cone line 24
  3. lemma OAI.DuffySimplex.cone_zero line 38
  4. lemma OAI.DuffySimplex.cone_succ line 39
  5. lemma OAI.DuffySimplex.continuous_cone line 42
  6. def OAI.DuffySimplex.toSimplex line 52
  7. lemma OAI.DuffySimplex.toSimplex_succ_zero line 62
  8. lemma OAI.DuffySimplex.toSimplex_succ_succ line 64
  9. lemma OAI.DuffySimplex.simplex_coordinate_le_one line 68
  10. lemma OAI.DuffySimplex.tail_sum line 72
  11. def OAI.DuffySimplex.tail line 77
  12. lemma OAI.DuffySimplex.cone_tail line 87
  13. lemma OAI.DuffySimplex.coordinate_zero_of_head_one line 98
  14. lemma OAI.DuffySimplex.cone_one line 104
  15. lemma OAI.DuffySimplex.surjective line 113
  16. lemma OAI.DuffySimplex.isQuotientMap line 129
  17. lemma OAI.DuffySimplex.boundary_iff line 132
  18. lemma OAI.DuffySimplex.injective_off_boundary line 158
  19. def OAI.DuffyBased.loop line 192
  20. lemma OAI.DuffyBased.loop_fiber line 195
  21. def OAI.DuffyBased.ofLoop line 203
  22. theorem OAI.DuffyBased.ofLoop_apply line 211
  23. theorem OAI.DuffyBased.loop_ofLoop line 215
  24. theorem OAI.DuffyBased.ofLoop_loop line 219
  25. def OAI.DuffyBased.equiv line 224
  26. def OAI.DuffyBased.homotopy line 231
  27. def OAI.DuffyBased.cylinder line 242
  28. lemma OAI.DuffyBased.cylinder_quotient line 246
  29. lemma OAI.DuffyBased.homotopy_fiber line 252
  30. def OAI.DuffyBased.homotopyOfLoop line 262
  31. def OAI.DuffyBased.homotopyClass line 284
  32. lemma OAI.DuffyBased.class_eq_iff line 287