OAI/GroupTheory/UniversalGroup/CellularAttachment.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalFInfinity.Cellular.transportedMap line 15
  2. lemma OAI.UniversalFInfinity.Cellular.transportedMap_apply line 18
  3. lemma OAI.UniversalFInfinity.Cellular.transportedMap_source line 21
  4. lemma OAI.UniversalFInfinity.Cellular.transportedMap_image line 27
  5. lemma OAI.UniversalFInfinity.Cellular.transportedMap_continuousOn line 31
  6. lemma OAI.UniversalFInfinity.Cellular.transportedMap_continuousOn_symm line 35
  7. def OAI.UniversalFInfinity.Cellular.transportCW line 46
  8. abbrev OAI.UniversalFInfinity.Attachment.OldCell line 101
  9. lemma OAI.UniversalFInfinity.Attachment.attaching_finite_frontier line 104
  10. abbrev OAI.UniversalFInfinity.Attachment.LayerCell line 125
  11. def OAI.UniversalFInfinity.Attachment.layerMap line 127
  12. lemma OAI.UniversalFInfinity.Attachment.layerMap_old_apply line 133
  13. lemma OAI.UniversalFInfinity.Attachment.layerMap_old_image line 137
  14. lemma OAI.UniversalFInfinity.Attachment.layerMap_new line 142
  15. def OAI.UniversalFInfinity.Attachment.layerCW line 146
  16. lemma OAI.UniversalFInfinity.Attachment.layerCW_dimensions line 264
  17. lemma OAI.UniversalFInfinity.Attachment.layerCW_finite_cells line 273
  18. instance OAI.UniversalFInfinity.Attachment.spaceMulAction line 290
  19. lemma OAI.UniversalFInfinity.Attachment.smul_base line 303
  20. lemma OAI.UniversalFInfinity.Attachment.smul_openCell line 304
  21. lemma OAI.UniversalFInfinity.Attachment.smul_cell line 309
  22. lemma OAI.UniversalFInfinity.Attachment.continuousConstSMul line 323
  23. lemma OAI.UniversalFInfinity.Attachment.isOpen_iff line 331
  24. abbrev OAI.UniversalFInfinity.Attachment.Collar line 342
  25. def OAI.UniversalFInfinity.Attachment.collarInclusion line 344
  26. def OAI.UniversalFInfinity.Attachment.radial line 346
  27. lemma OAI.UniversalFInfinity.Attachment.continuous_radial line 352
  28. lemma OAI.UniversalFInfinity.Attachment.collar_openEmbedding line 358
  29. lemma OAI.UniversalFInfinity.Attachment.radial_boundary line 361
  30. def OAI.UniversalFInfinity.Attachment.thickening line 370
  31. lemma OAI.UniversalFInfinity.Attachment.base_mem_thickening line 376
  32. lemma OAI.UniversalFInfinity.Attachment.cell_preimage_thickening line 379
  33. lemma OAI.UniversalFInfinity.Attachment.thickening_isOpen line 411
  34. lemma OAI.UniversalFInfinity.Attachment.thickening_disjoint line 421
  35. lemma OAI.UniversalFInfinity.Attachment.exists_disjoint_nhds line 435
  36. def OAI.UniversalFInfinity.Attachment.map line 464
  37. lemma OAI.UniversalFInfinity.Attachment.map_base line 469
  38. lemma OAI.UniversalFInfinity.Attachment.map_cell line 473
  39. lemma OAI.UniversalFInfinity.Attachment.map_openCell line 477
  40. lemma OAI.UniversalFInfinity.Attachment.map_surjective line 483
  41. lemma OAI.UniversalFInfinity.Attachment.map_isQuotientMap line 496
  42. def OAI.UniversalFInfinity.Attachment.FreeIndex line 521
  43. instance OAI.UniversalFInfinity.Attachment.(instance at line 523) line 523
  44. instance OAI.UniversalFInfinity.Attachment.(instance at line 528) line 528
  45. def OAI.UniversalFInfinity.Attachment.equivariantFamily line 536
  46. lemma OAI.UniversalFInfinity.Attachment.equivariantFamily_smul line 539
  47. instance OAI.UniversalFInfinity.Attachment.equivariantAttachmentContinuousAction line 542
  48. lemma OAI.UniversalFInfinity.Attachment.equivariantFamily_over line 550
  49. def OAI.UniversalFInfinity.Attachment.coverMap line 554
  50. lemma OAI.UniversalFInfinity.Attachment.coverMap_isQuotient line 557
  51. lemma OAI.UniversalFInfinity.Attachment.coverMap_fibers line 560
  52. lemma OAI.UniversalFInfinity.Attachment.coverMap_isQuotientCovering line 613
  53. lemma OAI.UniversalFInfinity.Attachment.coverMap_isCovering line 619