OAI/Algebra/GroupRing/Attachment.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.GroupRingTopology.Cellular.transportedMap line 16
  2. lemma OAI.GroupRingTopology.Cellular.transportedMap_apply line 19
  3. lemma OAI.GroupRingTopology.Cellular.transportedMap_source line 22
  4. lemma OAI.GroupRingTopology.Cellular.transportedMap_image line 28
  5. lemma OAI.GroupRingTopology.Cellular.transportedMap_continuousOn line 32
  6. lemma OAI.GroupRingTopology.Cellular.transportedMap_continuousOn_symm line 36
  7. def OAI.GroupRingTopology.Cellular.transportCW line 49

    Source documentation

    Closed embeddings transport classical CW structures, including their weak topology, with precisely the same cells.

    def transportCW : CWComplex (f '' C) where
…
  8. abbrev OAI.GroupRingTopology.Attachment.OldCell line 103
  9. lemma OAI.GroupRingTopology.Attachment.attaching_finite_frontier line 106
  10. abbrev OAI.GroupRingTopology.Attachment.LayerCell line 127
  11. def OAI.GroupRingTopology.Attachment.layerMap line 129
  12. lemma OAI.GroupRingTopology.Attachment.layerMap_old_apply line 135
  13. lemma OAI.GroupRingTopology.Attachment.layerMap_old_image line 139
  14. lemma OAI.GroupRingTopology.Attachment.layerMap_new line 144
  15. def OAI.GroupRingTopology.Attachment.layerCW line 148
  16. lemma OAI.GroupRingTopology.Attachment.layerCW_dimensions line 266
  17. lemma OAI.GroupRingTopology.Attachment.layerCW_finite_cells line 275
  18. instance OAI.GroupRingTopology.Attachment.spaceMulAction line 292
  19. lemma OAI.GroupRingTopology.Attachment.smul_base line 305
  20. lemma OAI.GroupRingTopology.Attachment.smul_openCell line 306
  21. lemma OAI.GroupRingTopology.Attachment.smul_cell line 311
  22. lemma OAI.GroupRingTopology.Attachment.continuousConstSMul line 325
  23. lemma OAI.GroupRingTopology.Attachment.isOpen_iff line 333
  24. abbrev OAI.GroupRingTopology.Attachment.Collar line 343
  25. def OAI.GroupRingTopology.Attachment.collarInclusion line 345
  26. def OAI.GroupRingTopology.Attachment.radial line 347
  27. lemma OAI.GroupRingTopology.Attachment.continuous_radial line 353
  28. lemma OAI.GroupRingTopology.Attachment.collar_openEmbedding line 359
  29. lemma OAI.GroupRingTopology.Attachment.radial_boundary line 362
  30. def OAI.GroupRingTopology.Attachment.thickening line 373

    Source documentation

    An open old-space neighborhood thickened by the outer half of each disk. Membership is tested by radial retraction of the disk to its attaching sphere.

    def thickening (U : Set X) : Set (Space a) := fun z =>
…

    Mentions: OAI.GroupRingTopology.Attachment.Space

  31. lemma OAI.GroupRingTopology.Attachment.base_mem_thickening line 379
  32. lemma OAI.GroupRingTopology.Attachment.cell_preimage_thickening line 382
  33. lemma OAI.GroupRingTopology.Attachment.thickening_isOpen line 414
  34. lemma OAI.GroupRingTopology.Attachment.thickening_disjoint line 424
  35. lemma OAI.GroupRingTopology.Attachment.exists_disjoint_nhds line 438