OAI/GroupTheory/UniversalGroup/TopologicalTowers.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.TopologicalTower.Space line 22
  2. def OAI.UniversalFInfinity.TopologicalTower.of line 24
  3. instance OAI.UniversalFInfinity.TopologicalTower.(instance at line 26) line 26
  4. lemma OAI.UniversalFInfinity.TopologicalTower.of_compat line 29
  5. lemma OAI.UniversalFInfinity.TopologicalTower.continuous_iff line 32
  6. lemma OAI.UniversalFInfinity.TopologicalTower.continuous_of line 37
  7. lemma OAI.UniversalFInfinity.TopologicalTower.isClosed_iff line 41
  8. lemma OAI.UniversalFInfinity.TopologicalTower.of_injective line 49
  9. lemma OAI.UniversalFInfinity.TopologicalTower.preimage_of_image_le line 53
  10. lemma OAI.UniversalFInfinity.TopologicalTower.preimage_of_image_ge line 65
  11. lemma OAI.UniversalFInfinity.TopologicalTower.of_closedEmbedding line 79
  12. def OAI.UniversalFInfinity.TopologicalTower.lift line 91
  13. lemma OAI.UniversalFInfinity.TopologicalTower.lift_of line 96
  14. def OAI.UniversalFInfinity.TopologicalTower.tailLift line 100
  15. lemma OAI.UniversalFInfinity.TopologicalTower.tailLift_of line 114
  16. def OAI.UniversalFInfinity.TopologicalTower.ExtendsReals line 123
  17. def OAI.UniversalFInfinity.TopologicalTower.realExtension line 128
  18. lemma OAI.UniversalFInfinity.TopologicalTower.realExtension_spec line 131
  19. def OAI.UniversalFInfinity.TopologicalTower.realFamily line 135
  20. lemma OAI.UniversalFInfinity.TopologicalTower.realFamily_self line 139
  21. lemma OAI.UniversalFInfinity.TopologicalTower.realFamily_compat line 142
  22. lemma OAI.UniversalFInfinity.TopologicalTower.exists_global_real_extension line 155
  23. lemma OAI.UniversalFInfinity.TopologicalTower.t2Space line 163
  24. lemma OAI.UniversalFInfinity.TopologicalTower.range_mono line 176
  25. lemma OAI.UniversalFInfinity.TopologicalTower.selection_closed line 183
  26. theorem OAI.UniversalFInfinity.TopologicalTower.compact_bounded line 201
  27. structure OAI.UniversalFInfinity.CellularTower.CellSystem line 242
  28. abbrev OAI.UniversalFInfinity.CellularTower.Limit line 254
  29. abbrev OAI.UniversalFInfinity.CellularTower.stage line 255
  30. def OAI.UniversalFInfinity.CellularTower.map line 257
  31. lemma OAI.UniversalFInfinity.CellularTower.map_eq_stage line 261
  32. lemma OAI.UniversalFInfinity.CellularTower.map_image line 267
  33. def OAI.UniversalFInfinity.CellularTower.globalIndex line 274
  34. lemma OAI.UniversalFInfinity.CellularTower.globalIndex_spec line 278
  35. lemma OAI.UniversalFInfinity.CellularTower.old_image line 282
  36. def OAI.UniversalFInfinity.CellularTower.cwComplex line 291
  37. lemma OAI.UniversalFInfinity.CellularTower.finite_cells line 349
  38. def OAI.UniversalFInfinity.Sequential.map line 360
  39. lemma OAI.UniversalFInfinity.Sequential.map_self line 363
  40. lemma OAI.UniversalFInfinity.Sequential.map_succ line 365
  41. lemma OAI.UniversalFInfinity.Sequential.map_step line 368
  42. instance OAI.UniversalFInfinity.Sequential.(instance at line 371) line 371
  43. lemma OAI.UniversalFInfinity.Sequential.map_closedEmbedding line 381
  44. structure OAI.UniversalFInfinity.Sequential.CellSteps line 389
  45. def OAI.UniversalFInfinity.Sequential.cellMap line 397
  46. lemma OAI.UniversalFInfinity.Sequential.cellMap_self line 401
  47. lemma OAI.UniversalFInfinity.Sequential.cellMap_succ line 403
  48. lemma OAI.UniversalFInfinity.Sequential.cellMap_injective line 406
  49. lemma OAI.UniversalFInfinity.Sequential.cellMap_comp line 411
  50. lemma OAI.UniversalFInfinity.Sequential.cellMap_compat line 419
  51. lemma OAI.UniversalFInfinity.Sequential.cellMap_exhaustive line 428
  52. def OAI.UniversalFInfinity.Sequential.cellSystem line 446