OAI/GroupTheory/UniversalGroup/HomotopyProducts.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.HomotopyFunctor.loopMap line 18
  2. lemma OAI.UniversalFInfinity.HomotopyFunctor.loopMap_homotopic line 21
  3. def OAI.UniversalFInfinity.HomotopyFunctor.map line 25
  4. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_mk line 28
  5. lemma OAI.UniversalFInfinity.HomotopyFunctor.loopMap_const line 31
  6. lemma OAI.UniversalFInfinity.HomotopyFunctor.loopMap_transAt line 36
  7. def OAI.UniversalFInfinity.HomotopyFunctor.mapHom line 44
  8. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_id line 57
  9. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_comp line 61
  10. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_const line 68
  11. def OAI.UniversalFInfinity.HomotopyFunctor.loopPair line 75
  12. lemma OAI.UniversalFInfinity.HomotopyFunctor.pair_homotopic line 78
  13. lemma OAI.UniversalFInfinity.HomotopyFunctor.product_ext line 87
  14. lemma OAI.UniversalFInfinity.HomotopyFunctor.diagonal_split line 96
  15. theorem OAI.UniversalFInfinity.HomotopyFunctor.product_additivity line 146
  16. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_eq_of_homotopy line 161
  17. abbrev OAI.UniversalFInfinity.Milnor.Shapes line 180
  18. def OAI.UniversalFInfinity.Milnor.basedShapes line 181
  19. def OAI.UniversalFInfinity.Milnor.stage line 182
  20. lemma OAI.UniversalFInfinity.Milnor.stage_mono line 184
  21. lemma OAI.UniversalFInfinity.Milnor.stage_point_face line 187
  22. def OAI.UniversalFInfinity.Milnor.stagePoint line 192
  23. def OAI.UniversalFInfinity.Milnor.stageIncl line 196
  24. lemma OAI.UniversalFInfinity.Milnor.stageIncl_point line 199
  25. def OAI.UniversalFInfinity.Milnor.stageHom line 202
  26. instance OAI.UniversalFInfinity.Milnor.(instance at line 207) line 207
  27. instance OAI.UniversalFInfinity.Milnor.(instance at line 223) line 223
  28. instance OAI.UniversalFInfinity.Milnor.(instance at line 238) line 238
  29. lemma OAI.UniversalFInfinity.Milnor.smul_weight line 241
  30. lemma OAI.UniversalFInfinity.Milnor.smul_weight_inv line 249
  31. lemma OAI.UniversalFInfinity.Milnor.exists_disjoint_nhds line 252
  32. lemma OAI.UniversalFInfinity.Milnor.quotientCovering line 271
  33. abbrev OAI.UniversalFInfinity.Milnor.Stage line 285
  34. def OAI.UniversalFInfinity.Milnor.stageFull line 287
  35. lemma OAI.UniversalFInfinity.Milnor.stageFull_embedding line 289
  36. lemma OAI.UniversalFInfinity.Milnor.stage_translate line 292
  37. def OAI.UniversalFInfinity.Milnor.stageSmul line 295
  38. instance OAI.UniversalFInfinity.Milnor.stageAction line 298
  39. instance OAI.UniversalFInfinity.Milnor.stageContinuousAction line 314
  40. lemma OAI.UniversalFInfinity.Milnor.stageFull_smul line 317
  41. lemma OAI.UniversalFInfinity.Milnor.stageIncl_smul line 319
  42. lemma OAI.UniversalFInfinity.Milnor.compact_controlled line 322
  43. lemma OAI.UniversalFInfinity.Milnor.compact_orbit_controlled line 332
  44. def OAI.UniversalFInfinity.Milnor.CompactFundamentalSet line 343
  45. lemma OAI.UniversalFInfinity.Milnor.equivariant_controlled line 346
  46. def OAI.UniversalFInfinity.Milnor.factorStage line 357
  47. lemma OAI.UniversalFInfinity.Milnor.factorStage_spec line 365
  48. lemma OAI.UniversalFInfinity.Milnor.factorStage_smul line 368