OAI/GroupTheory/UniversalGroup/Attachments.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.Attachment.Disk line 11
  2. abbrev OAI.UniversalFInfinity.Attachment.Sphere line 12
  3. abbrev OAI.UniversalFInfinity.Attachment.OpenDisk line 13
  4. def OAI.UniversalFInfinity.Attachment.boundary line 15
  5. def OAI.UniversalFInfinity.Attachment.interior line 17
  6. lemma OAI.UniversalFInfinity.Attachment.continuous_boundary line 19
  7. lemma OAI.UniversalFInfinity.Attachment.continuous_interior line 21
  8. lemma OAI.UniversalFInfinity.Attachment.boundary_closedEmbedding line 23
  9. def OAI.UniversalFInfinity.Attachment.Space line 29
  10. def OAI.UniversalFInfinity.Attachment.quotient line 31
  11. instance OAI.UniversalFInfinity.Attachment.(instance at line 43) line 43
  12. lemma OAI.UniversalFInfinity.Attachment.quotient_inl line 45
  13. lemma OAI.UniversalFInfinity.Attachment.quotient_interior line 47
  14. lemma OAI.UniversalFInfinity.Attachment.quotient_boundary line 52
  15. lemma OAI.UniversalFInfinity.Attachment.quotient_surjective line 60
  16. lemma OAI.UniversalFInfinity.Attachment.continuous_quotient line 66
  17. def OAI.UniversalFInfinity.Attachment.base line 68
  18. def OAI.UniversalFInfinity.Attachment.cell line 69
  19. lemma OAI.UniversalFInfinity.Attachment.continuous_base line 72
  20. lemma OAI.UniversalFInfinity.Attachment.cell_boundary line 75
  21. lemma OAI.UniversalFInfinity.Attachment.cell_interior line 77
  22. lemma OAI.UniversalFInfinity.Attachment.continuous_iff line 80
  23. lemma OAI.UniversalFInfinity.Attachment.isClosed_iff line 86
  24. lemma OAI.UniversalFInfinity.Attachment.cell_preimage_base_image line 92
  25. lemma OAI.UniversalFInfinity.Attachment.base_isClosedMap line 122
  26. lemma OAI.UniversalFInfinity.Attachment.base_closedEmbedding line 133
  27. def OAI.UniversalFInfinity.Attachment.lift line 137
  28. lemma OAI.UniversalFInfinity.Attachment.lift_base line 156
  29. lemma OAI.UniversalFInfinity.Attachment.lift_cell line 160
  30. lemma OAI.UniversalFInfinity.Attachment.lift_unique line 175
  31. lemma OAI.UniversalFInfinity.Attachment.interior_openEmbedding line 184
  32. def OAI.UniversalFInfinity.Attachment.openCell line 187
  33. lemma OAI.UniversalFInfinity.Attachment.openCell_eq line 189
  34. lemma OAI.UniversalFInfinity.Attachment.quotient_preimage_openCell_image line 193
  35. lemma OAI.UniversalFInfinity.Attachment.openCell_openEmbedding line 241
  36. lemma OAI.UniversalFInfinity.Attachment.exists_real_extension line 252
  37. def OAI.UniversalFInfinity.Attachment.RealSeparated line 261
  38. lemma OAI.UniversalFInfinity.Attachment.RealSeparated.t2Space line 264
  39. lemma OAI.UniversalFInfinity.Attachment.realSeparated_of_tychonoff line 271
  40. lemma OAI.UniversalFInfinity.Attachment.exists_interior_separator line 281
  41. lemma OAI.UniversalFInfinity.Attachment.realSeparated line 344
  42. lemma OAI.UniversalFInfinity.Attachment.t2Space line 372
  43. def OAI.UniversalFInfinity.Attachment.characteristic line 377
  44. lemma OAI.UniversalFInfinity.Attachment.characteristic_disk line 381
  45. lemma OAI.UniversalFInfinity.Attachment.characteristic_open line 385
  46. lemma OAI.UniversalFInfinity.Attachment.characteristic_bijOn line 389
  47. def OAI.UniversalFInfinity.Attachment.characteristicPE line 402
  48. lemma OAI.UniversalFInfinity.Attachment.characteristicPE_continuousOn line 405
  49. lemma OAI.UniversalFInfinity.Attachment.characteristicPE_continuousOn_symm line 414
  50. lemma OAI.UniversalFInfinity.Attachment.characteristicPE_image_ball line 428
  51. lemma OAI.UniversalFInfinity.Attachment.characteristicPE_image_closedBall line 432
  52. abbrev OAI.UniversalFInfinity.Attachment.CellIndex line 441
  53. def OAI.UniversalFInfinity.Attachment.cellMap line 443
  54. def OAI.UniversalFInfinity.Attachment.relCWComplex line 450