OAI/GroupTheory/UniversalGroup/CellularFillings.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniversalFInfinity.Cellular.exists_equivariant_cellular_homotopy line 37
  2. def OAI.UniversalFInfinity.Cellular.LowFillable line 87
  3. lemma OAI.UniversalFInfinity.Cellular.pathEndpoint_lift_at line 90
  4. lemma OAI.UniversalFInfinity.Cellular.equivariant_low_homotopy line 109
  5. def OAI.UniversalFInfinity.Cellular.brownObstructions line 154
  6. abbrev OAI.UniversalFInfinity.Cellular.BrownAttachment line 158
  7. def OAI.UniversalFInfinity.Cellular.brownBase line 161
  8. lemma OAI.UniversalFInfinity.Cellular.brown_map_extension line 165
  9. lemma OAI.UniversalFInfinity.Cellular.brown_homotopy_extension line 181
  10. lemma OAI.UniversalFInfinity.Cellular.fill_through_next_skeleton line 226
  11. lemma OAI.UniversalFInfinity.Cellular.filling_after_skeletal_domination line 246
  12. lemma OAI.UniversalFInfinity.Attachment.lowFillable_of_kills_old line 263
  13. lemma OAI.UniversalFInfinity.Cellular.brown_lowFillable line 305
  14. lemma OAI.UniversalFInfinity.Cellular.controlled_map_on_skeleton line 350
  15. lemma OAI.UniversalFInfinity.Cellular.exists_brown_data line 361
  16. lemma OAI.UniversalFInfinity.Cellular.skeleton_eq_univ_of_dimension line 435
  17. lemma OAI.UniversalFInfinity.Cellular.exists_finite_brown_attachment line 447
  18. abbrev OAI.UniversalFInfinity.Attachment.LayerOrbits line 476
  19. def OAI.UniversalFInfinity.Attachment.layerEquiv line 478
  20. lemma OAI.UniversalFInfinity.Attachment.layerEquiv_map_disk line 497
  21. lemma OAI.UniversalFInfinity.Attachment.layerEquiv_image line 518
  22. def OAI.UniversalFInfinity.Attachment.equivariantLayerCW line 531
  23. lemma OAI.UniversalFInfinity.Attachment.equivariantLayerCW_dims line 537
  24. lemma OAI.UniversalFInfinity.Attachment.equivariantLayerCW_smul line 540
  25. def OAI.UniversalFInfinity.Attachment.layerOld line 548
  26. lemma OAI.UniversalFInfinity.Attachment.layerOld_injective line 552
  27. lemma OAI.UniversalFInfinity.Attachment.layerOld_map line 559
  28. lemma OAI.UniversalFInfinity.Attachment.layerOld_exhaustive line 566