OAI/GroupTheory/UniversalGroup/MilnorProducts.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Simplicial.restrict line 23
  2. lemma OAI.UniversalFInfinity.Simplicial.restrict_le line 30
  3. instance OAI.UniversalFInfinity.Simplicial.finiteFace_restrict line 31
  4. def OAI.UniversalFInfinity.Simplicial.restrictInclusion line 39
  5. lemma OAI.UniversalFInfinity.Simplicial.compactMap_finiteRestriction line 42
  6. abbrev OAI.UniversalFInfinity.Milnor.StagePi line 63
  7. abbrev OAI.UniversalFInfinity.Milnor.StageValues line 64
  8. def OAI.UniversalFInfinity.Milnor.valueHom line 66
  9. instance OAI.UniversalFInfinity.Milnor.(instance at line 71) line 71
  10. abbrev OAI.UniversalFInfinity.Milnor.ControlledValues line 75
  11. def OAI.UniversalFInfinity.Milnor.value line 77
  12. lemma OAI.UniversalFInfinity.Milnor.value_eq_of_le line 79
  13. lemma OAI.UniversalFInfinity.Milnor.value_eq_one_iff line 82
  14. lemma OAI.UniversalFInfinity.Milnor.value_mul line 86
  15. def OAI.UniversalFInfinity.Milnor.stageMap line 102
  16. lemma OAI.UniversalFInfinity.Milnor.stageMap_point line 105
  17. def OAI.UniversalFInfinity.Milnor.stageMapHom line 113
  18. def OAI.UniversalFInfinity.Milnor.stageMapValue line 115
  19. lemma OAI.UniversalFInfinity.Milnor.stageMapValue_congrTarget line 118
  20. lemma OAI.UniversalFInfinity.Milnor.stageMapValue_eq_of_homotopy line 131
  21. lemma OAI.UniversalFInfinity.Milnor.image_stage_valid line 140
  22. def OAI.UniversalFInfinity.Milnor.mapValue line 144
  23. lemma OAI.UniversalFInfinity.Milnor.mapValue_eq line 147
  24. lemma OAI.UniversalFInfinity.Milnor.relayerStageLeftValid line 162
  25. lemma OAI.UniversalFInfinity.Milnor.relayerStageRightValid line 166
  26. def OAI.UniversalFInfinity.Milnor.relayerToStage line 170
  27. def OAI.UniversalFInfinity.Milnor.relayerStageHomotopy line 174
  28. lemma OAI.UniversalFInfinity.Milnor.relayerStageHomotopy_fixed line 180
  29. lemma OAI.UniversalFInfinity.Milnor.mapValue_relayer line 187
  30. lemma OAI.UniversalFInfinity.Simplicial.loop_finite_restriction line 203
  31. def OAI.UniversalFInfinity.Simplicial.tensor line 228
  32. lemma OAI.UniversalFInfinity.Simplicial.tensor_apply line 234
  33. lemma OAI.UniversalFInfinity.Simplicial.tensor_support line 235
  34. lemma OAI.UniversalFInfinity.Simplicial.tensor_sum line 239
  35. def OAI.UniversalFInfinity.Simplicial.pairMap line 248
  36. lemma OAI.UniversalFInfinity.Simplicial.pairMap_support line 258
  37. lemma OAI.UniversalFInfinity.Simplicial.continuous_pairMap_faces line 262
  38. instance OAI.UniversalFInfinity.Simplicial.(instance at line 293) line 293
  39. lemma OAI.UniversalFInfinity.Simplicial.continuous_prod_faces_iff line 302
  40. lemma OAI.UniversalFInfinity.Simplicial.continuous_pairMap line 318
  41. def OAI.UniversalFInfinity.Simplicial.pairMapC line 321
  42. def OAI.UniversalFInfinity.Simplicial.carrierBlend line 335
  43. lemma OAI.UniversalFInfinity.Simplicial.continuous_carrierBlend line 339
  44. def OAI.UniversalFInfinity.Simplicial.carrierHomotopy line 354
  45. lemma OAI.UniversalFInfinity.Simplicial.carrierHomotopy_fixed line 360
  46. lemma OAI.UniversalFInfinity.Simplicial.tensor_single line 373
  47. lemma OAI.UniversalFInfinity.Simplicial.diagonal_face line 391
  48. def OAI.UniversalFInfinity.Simplicial.productDiagonal line 398
  49. def OAI.UniversalFInfinity.Simplicial.vertexDiagonal line 400
  50. def OAI.UniversalFInfinity.Simplicial.diagonalCarrier line 402
  51. lemma OAI.UniversalFInfinity.Simplicial.productDiagonal_carried line 403
  52. lemma OAI.UniversalFInfinity.Simplicial.vertexDiagonal_carried line 407
  53. def OAI.UniversalFInfinity.Simplicial.diagonalHomotopy line 414
  54. lemma OAI.UniversalFInfinity.Simplicial.pairMap_pure line 419
  55. lemma OAI.UniversalFInfinity.Simplicial.diagonalHomotopy_fixed line 427
  56. lemma OAI.UniversalFInfinity.Simplicial.tensor_single_right_push line 442
  57. lemma OAI.UniversalFInfinity.Simplicial.tensor_single_left_push line 452