OAI/GroupTheory/FiniteType/TwistedBrin.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TwistedBrin.finite_local_cover line 21
  2. lemma OAI.TwistedBrin.finite_grid_refinement line 36
  3. lemma OAI.TwistedBrin.hasTable_of_isLocal line 54
  4. lemma OAI.TwistedBrin.hasTable_iff_isLocal line 101
  5. lemma OAI.TwistedBrin.locallyStandard_id line 105
  6. lemma OAI.TwistedBrin.locallyStandard_comp line 107
  7. structure OAI.TwistedBrin.LocalEmbedding line 139
  8. instance OAI.TwistedBrin.LocalEmbedding.(instance at line 143) line 143
  9. lemma OAI.TwistedBrin.LocalEmbedding.ext line 144
  10. lemma OAI.TwistedBrin.LocalEmbedding.injective line 149
  11. def OAI.TwistedBrin.LocalEmbedding.identity line 151
  12. lemma OAI.TwistedBrin.LocalEmbedding.identity_apply line 155
  13. def OAI.TwistedBrin.LocalEmbedding.comp line 157
  14. lemma OAI.TwistedBrin.LocalEmbedding.comp_apply line 163
  15. lemma OAI.TwistedBrin.LocalEmbedding.comp_assoc line 164
  16. lemma OAI.TwistedBrin.LocalEmbedding.identity_comp line 165
  17. lemma OAI.TwistedBrin.LocalEmbedding.comp_identity line 166
  18. def OAI.TwistedBrin.LocalEmbedding.ofPrefix line 168
  19. lemma OAI.TwistedBrin.LocalEmbedding.ofPrefix_apply line 175
  20. def OAI.TwistedBrin.LocalEmbedding.global line 177
  21. lemma OAI.TwistedBrin.LocalEmbedding.global_apply line 182
  22. lemma OAI.TwistedBrin.LocalEmbedding.global_one line 183
  23. lemma OAI.TwistedBrin.LocalEmbedding.global_mul line 184
  24. def OAI.TwistedBrin.LocalEmbedding.ofGroup line 189
  25. lemma OAI.TwistedBrin.LocalEmbedding.ofGroup_apply line 192
  26. def OAI.TwistedBrin.LocalEmbedding.Gauge line 194
  27. lemma OAI.TwistedBrin.LocalEmbedding.gauge_refl line 196
  28. lemma OAI.TwistedBrin.LocalEmbedding.gauge_symm line 198
  29. lemma OAI.TwistedBrin.LocalEmbedding.gauge_trans line 203
  30. instance OAI.TwistedBrin.LocalEmbedding.gaugeSetoid line 211
  31. lemma OAI.TwistedBrin.LocalEmbedding.gauge_range_eq line 215
  32. lemma OAI.TwistedBrin.LocalEmbedding.gauge_comp_left line 220
  33. def OAI.TwistedBrin.GermBrick line 227
  34. def OAI.TwistedBrin.GermBrick.mk line 231
  35. def OAI.TwistedBrin.GermBrick.region line 233
  36. lemma OAI.TwistedBrin.GermBrick.region_mk line 235
  37. lemma OAI.TwistedBrin.GermBrick.region_nonempty line 237
  38. def OAI.TwistedBrin.GermBrick.map line 241
  39. lemma OAI.TwistedBrin.GermBrick.map_mk line 243
  40. lemma OAI.TwistedBrin.GermBrick.map_identity line 245
  41. lemma OAI.TwistedBrin.GermBrick.map_comp line 249
  42. lemma OAI.TwistedBrin.GermBrick.region_map line 253
  43. lemma OAI.TwistedBrin.LocalEmbedding.ofGroup_one line 264
  44. lemma OAI.TwistedBrin.LocalEmbedding.ofGroup_mul line 265
  45. lemma OAI.TwistedBrin.LocalEmbedding.ofPrefix_empty line 267
  46. lemma OAI.TwistedBrin.LocalEmbedding.ofPrefix_append line 268
  47. lemma OAI.TwistedBrin.LocalEmbedding.global_ofPrefix line 273
  48. def OAI.TwistedBrin.GermBrick.representative line 283
  49. lemma OAI.TwistedBrin.GermBrick.mk_representative line 284
  50. lemma OAI.TwistedBrin.GermBrick.mk_eq_iff line 285
  51. lemma OAI.TwistedBrin.GermBrick.mk_gauge line 287
  52. def OAI.TwistedBrin.GermBrick.groupEquiv line 291
  53. lemma OAI.TwistedBrin.GermBrick.groupEquiv_apply line 299
  54. def OAI.TwistedBrin.GermBrick.action line 302
  55. lemma OAI.TwistedBrin.GermBrick.region_groupEquiv line 312
  56. def OAI.TwistedBrin.GermBrick.Restricts line 315
  57. lemma OAI.TwistedBrin.GermBrick.restricts_refl line 319
  58. lemma OAI.TwistedBrin.GermBrick.restricts_trans line 322
  59. lemma OAI.TwistedBrin.GermBrick.region_subset_of_restricts line 335
  60. lemma OAI.TwistedBrin.GermBrick.restricts_map line 341
  61. lemma OAI.TwistedBrin.GermBrick.restricts_prefix line 346
  62. structure OAI.TwistedBrin.Basis line 353
  63. instance OAI.TwistedBrin.Basis.(instance at line 359) line 359
  64. instance OAI.TwistedBrin.Basis.(instance at line 360) line 360
  65. def OAI.TwistedBrin.Basis.rank line 362
  66. def OAI.TwistedBrin.Basis.chart line 364
  67. lemma OAI.TwistedBrin.Basis.chart_region line 366
  68. def OAI.TwistedBrin.Basis.evaluate line 370
  69. lemma OAI.TwistedBrin.Basis.evaluate_bijective line 372
  70. def OAI.TwistedBrin.Basis.equivalence line 392
  71. lemma OAI.TwistedBrin.Basis.equivalence_apply line 395
  72. def OAI.TwistedBrin.Basis.trivial line 398
  73. def OAI.TwistedBrin.Basis.translate line 405
  74. lemma OAI.TwistedBrin.Basis.rank_translate line 431
  75. def OAI.TwistedBrin.Basis.Refines line 434
  76. lemma OAI.TwistedBrin.Basis.refines_refl line 437
  77. lemma OAI.TwistedBrin.Basis.refines_trans line 438