OAI/GroupTheory/UniversalGroup/BrownConstruction.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniversalFInfinity.Brown.Stage line 24
  2. instance OAI.UniversalFInfinity.Brown.(instance at line 52) line 52
  3. instance OAI.UniversalFInfinity.Brown.(instance at line 53) line 53
  4. def OAI.UniversalFInfinity.Brown.ZeroOrbits line 57
  5. instance OAI.UniversalFInfinity.Brown.(instance at line 60) line 60
  6. def OAI.UniversalFInfinity.Brown.zeroEquiv line 64
  7. lemma OAI.UniversalFInfinity.Brown.zeroEquiv_map line 74
  8. lemma OAI.UniversalFInfinity.Brown.discrete_dim line 79
  9. def OAI.UniversalFInfinity.Brown.pointCover line 85
  10. lemma OAI.UniversalFInfinity.Brown.pointCover_quotient line 86
  11. def OAI.UniversalFInfinity.Brown.zeroStage line 103
  12. def OAI.UniversalFInfinity.Brown.nextIndex line 143
  13. instance OAI.UniversalFInfinity.Brown.(instance at line 144) line 144
  14. def OAI.UniversalFInfinity.Brown.attaching line 147
  15. lemma OAI.UniversalFInfinity.Brown.attaching_fill line 149
  16. def OAI.UniversalFInfinity.Brown.downstairs line 152
  17. instance OAI.UniversalFInfinity.Brown.nextE_nonempty line 154
  18. instance OAI.UniversalFInfinity.Brown.nextB_nonempty line 156
  19. instance OAI.UniversalFInfinity.Brown.nextE_t2 line 157
  20. instance OAI.UniversalFInfinity.Brown.nextB_t2 line 159
  21. def OAI.UniversalFInfinity.Brown.nextStage line 161
  22. def OAI.UniversalFInfinity.Brown.nextInE line 194
  23. def OAI.UniversalFInfinity.Brown.nextInB line 195
  24. lemma OAI.UniversalFInfinity.Brown.nextInE_closed line 196
  25. lemma OAI.UniversalFInfinity.Brown.nextInB_closed line 197
  26. lemma OAI.UniversalFInfinity.Brown.nextInE_smul line 198
  27. lemma OAI.UniversalFInfinity.Brown.next_square line 199
  28. def OAI.UniversalFInfinity.Brown.nextCellE line 202
  29. lemma OAI.UniversalFInfinity.Brown.nextCellE_injective line 204
  30. lemma OAI.UniversalFInfinity.Brown.nextCellE_exhaustive line 206
  31. lemma OAI.UniversalFInfinity.Brown.nextCellE_map line 208
  32. def OAI.UniversalFInfinity.Brown.nextCellB line 212
  33. lemma OAI.UniversalFInfinity.Brown.nextCellB_injective line 213
  34. lemma OAI.UniversalFInfinity.Brown.nextCellB_exhaustive line 214
  35. lemma OAI.UniversalFInfinity.Brown.nextCellB_map line 219
  36. lemma OAI.UniversalFInfinity.Brown.nextE_extendsReal line 222
  37. lemma OAI.UniversalFInfinity.Brown.nextB_extendsReal line 224
  38. lemma OAI.UniversalFInfinity.Brown.nextE_extendsSlice line 226
  39. def OAI.UniversalFInfinity.Brown.stages line 240
  40. abbrev OAI.UniversalFInfinity.Brown.E line 243
  41. abbrev OAI.UniversalFInfinity.Brown.B line 244
  42. def OAI.UniversalFInfinity.Brown.eStep line 246
  43. def OAI.UniversalFInfinity.Brown.bStep line 247
  44. abbrev OAI.UniversalFInfinity.Brown.eMap line 248
  45. abbrev OAI.UniversalFInfinity.Brown.bMap line 249
  46. lemma OAI.UniversalFInfinity.Brown.eMap_closed line 250
  47. lemma OAI.UniversalFInfinity.Brown.bMap_closed line 252
  48. instance OAI.UniversalFInfinity.Brown.(instance at line 255) line 255
  49. def OAI.UniversalFInfinity.Brown.eCells line 265
  50. def OAI.UniversalFInfinity.Brown.bCells line 271
  51. abbrev OAI.UniversalFInfinity.Brown.Total line 278
  52. abbrev OAI.UniversalFInfinity.Brown.Base line 279
  53. instance OAI.UniversalFInfinity.Brown.(instance at line 280) line 280
  54. instance OAI.UniversalFInfinity.Brown.(instance at line 281) line 281
  55. lemma OAI.UniversalFInfinity.Brown.e_extendsReal line 283
  56. lemma OAI.UniversalFInfinity.Brown.b_extendsReal line 290
  57. instance OAI.UniversalFInfinity.Brown.totalT2 line 297
  58. instance OAI.UniversalFInfinity.Brown.baseT2 line 299
  59. instance OAI.UniversalFInfinity.Brown.totalCW line 301
  60. instance OAI.UniversalFInfinity.Brown.baseCW line 303
  61. lemma OAI.UniversalFInfinity.Brown.base_finite line 305
  62. lemma OAI.UniversalFInfinity.Brown.eventually_fills line 308
  63. instance OAI.UniversalFInfinity.Brown.totalContractible line 314
  64. lemma OAI.UniversalFInfinity.Brown.e_extendsSlices line 317
  65. def OAI.UniversalFInfinity.Brown.pStage line 324
  66. lemma OAI.UniversalFInfinity.Brown.p_compat line 325
  67. def OAI.UniversalFInfinity.Brown.pLimit line 334
  68. lemma OAI.UniversalFInfinity.Brown.pLimit_covering line 336
  69. instance OAI.UniversalFInfinity.Brown.baseConnected line 340
  70. theorem OAI.UniversalFInfinity.Brown.geometric_of_uniform line 345