OAI/GroupTheory/UniversalGroup/SimplicialProducts.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Milnor.pairVertex line 24
  2. def OAI.UniversalFInfinity.Milnor.pairFace line 27
  3. lemma OAI.UniversalFInfinity.Milnor.pairFace_valid line 30
  4. lemma OAI.UniversalFInfinity.Milnor.pairFace_mono line 41
  5. lemma OAI.UniversalFInfinity.Milnor.pair_translate_vertex line 49
  6. lemma OAI.UniversalFInfinity.Milnor.pairFace_translate line 61
  7. def OAI.UniversalFInfinity.Milnor.productShapes line 78
  8. lemma OAI.UniversalFInfinity.Milnor.pairFace_controlled line 82
  9. lemma OAI.UniversalFInfinity.HomotopyFunctor.map_congr_maps line 96
  10. lemma OAI.UniversalFInfinity.Simplicial.anchorFace line 115
  11. lemma OAI.UniversalFInfinity.Simplicial.leftAxisFace line 120
  12. lemma OAI.UniversalFInfinity.Simplicial.rightAxisFace line 125
  13. def OAI.UniversalFInfinity.Simplicial.leftAxis line 130
  14. def OAI.UniversalFInfinity.Simplicial.rightAxis line 131
  15. lemma OAI.UniversalFInfinity.Simplicial.leftAxis_point line 133
  16. lemma OAI.UniversalFInfinity.Simplicial.rightAxis_point line 137
  17. lemma OAI.UniversalFInfinity.Simplicial.pairLeft_eq line 143
  18. lemma OAI.UniversalFInfinity.Simplicial.pairRight_eq line 150
  19. lemma OAI.UniversalFInfinity.Simplicial.productDiagonal_point line 159
  20. lemma OAI.UniversalFInfinity.Simplicial.finite_pair_additivity line 166
  21. lemma OAI.UniversalFInfinity.Simplicial.finite_pair_additivity_to line 192
  22. lemma OAI.UniversalFInfinity.Simplicial.pair_additivity line 200
  23. lemma OAI.UniversalFInfinity.Simplicial.pair_additivity_to line 220
  24. def OAI.UniversalFInfinity.Milnor.commutingProduct line 240
  25. def OAI.UniversalFInfinity.Milnor.addTarget line 245
  26. def OAI.UniversalFInfinity.Milnor.addVertex line 246
  27. lemma OAI.UniversalFInfinity.Milnor.addValid line 248
  28. def OAI.UniversalFInfinity.Milnor.diagLayer line 251
  29. def OAI.UniversalFInfinity.Milnor.leftLayer line 252
  30. def OAI.UniversalFInfinity.Milnor.rightLayer line 253
  31. lemma OAI.UniversalFInfinity.Milnor.diagLayer_injective line 254
  32. lemma OAI.UniversalFInfinity.Milnor.leftLayer_injective line 255
  33. lemma OAI.UniversalFInfinity.Milnor.rightLayer_injective line 256
  34. lemma OAI.UniversalFInfinity.Milnor.addDiagValid line 258
  35. lemma OAI.UniversalFInfinity.Milnor.addLeftValid line 262
  36. lemma OAI.UniversalFInfinity.Milnor.addRightValid line 268
  37. lemma OAI.UniversalFInfinity.Milnor.addLeftMap line 274
  38. lemma OAI.UniversalFInfinity.Milnor.addRightMap line 283
  39. lemma OAI.UniversalFInfinity.Milnor.addHom line 293
  40. theorem OAI.UniversalFInfinity.Milnor.mapValue_product line 308