OAI/GroupTheory/UniversalGroup/ControlledCells.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.UniversalFInfinity.Cellular.square_filling_after line 25
  2. def OAI.UniversalFInfinity.Cellular.postPath line 122
  3. structure OAI.UniversalFInfinity.Cellular.SquareBoundary line 125
  4. def OAI.UniversalFInfinity.Cellular.SquareBoundary.post line 133
  5. structure OAI.UniversalFInfinity.Cellular.PartialSquare line 148
  6. def OAI.UniversalFInfinity.Cellular.PartialSquare.onSphere line 159
  7. lemma OAI.UniversalFInfinity.Cellular.PartialSquare.cell_extension_after line 165
  8. def OAI.UniversalFInfinity.Cellular.PartialSquare.next line 183
  9. def OAI.UniversalFInfinity.Cellular.PartialSquare.start line 218
  10. def OAI.UniversalFInfinity.Cellular.PartialSquare.toMap line 228
  11. def OAI.UniversalFInfinity.Cellular.boundaryTower line 246
  12. def OAI.UniversalFInfinity.Cellular.squareTower line 252
  13. theorem OAI.UniversalFInfinity.Cellular.exists_tower_square line 258
  14. lemma OAI.UniversalFInfinity.SphereTopology.parametric_extension line 279
  15. def OAI.UniversalFInfinity.Cellular.familyCylinderFace line 328
  16. def OAI.UniversalFInfinity.Cellular.familyFaceMap line 331
  17. lemma OAI.UniversalFInfinity.Cellular.familyFaceMap_eq line 347
  18. lemma OAI.UniversalFInfinity.Cellular.familyCylinder_continuous line 354
  19. lemma OAI.UniversalFInfinity.Cellular.family_cylinder_filling line 385
  20. lemma OAI.UniversalFInfinity.Cellular.family_square_filling line 438
  21. lemma OAI.UniversalFInfinity.Cellular.SquareBoundary.fill_after_nullhomotopy line 527
  22. def OAI.UniversalFInfinity.Cellular.contractionPath line 558
  23. def OAI.UniversalFInfinity.Cellular.connectorTop line 564
  24. def OAI.UniversalFInfinity.Cellular.connectorSquare line 567
  25. lemma OAI.UniversalFInfinity.Cellular.connector_after_nullhomotopy line 578