OAI/GroupTheory/FiniteType/LoopPath.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LoopPath.fromPath line 27
  2. lemma OAI.LoopPath.fromPath_apply line 41
  3. lemma OAI.LoopPath.fromPath_trans line 44
  4. def OAI.LoopPath.fromHomotopy line 61
  5. def OAI.SimplexAddition.basedFace line 92
  6. lemma OAI.SimplexAddition.loop_face line 101
  7. theorem OAI.SimplexAddition.three_face line 110
  8. abbrev OAI.SimplexHorn.Std line 131
  9. abbrev OAI.SimplexHorn.Horn line 134
  10. def OAI.SimplexHorn.minimum line 136
  11. lemma OAI.SimplexHorn.minimum_nonneg line 139
  12. lemma OAI.SimplexHorn.minimum_le line 142
  13. lemma OAI.SimplexHorn.minimum_attained line 146
  14. lemma OAI.SimplexHorn.minimum_eq_zero line 152
  15. lemma OAI.SimplexHorn.continuous_minimum line 157
  16. def OAI.SimplexHorn.retract line 161
  17. lemma OAI.SimplexHorn.retract_self line 184
  18. lemma OAI.SimplexHorn.retract_succAbove line 187
  19. lemma OAI.SimplexHorn.retract_mem line 190
  20. lemma OAI.SimplexHorn.retract_fix line 195
  21. lemma OAI.SimplexHorn.continuous_retract line 203
  22. def OAI.SimplexHorn.retraction line 214
  23. abbrev OAI.SimplexHorn.Faces line 217
  24. def OAI.SimplexHorn.quotient line 219
  25. lemma OAI.SimplexHorn.quotient_surjective line 223
  26. lemma OAI.SimplexHorn.quotient_isQuotientMap line 228
  27. def OAI.SimplexHorn.glue line 234
  28. lemma OAI.SimplexHorn.glue_face line 240
  29. def OAI.SimplexHorn.fill line 248
  30. lemma OAI.SimplexHorn.fill_face line 252