OAI/GroupTheory/FiniteType/TwistedBrinEquiv.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwistedBrin.PartitionMaps.equiv line 14
  2. lemma OAI.TwistedBrin.PartitionMaps.equiv_apply line 26
  3. def OAI.TwistedBrin.PartitionMaps.rearrange line 29
  4. lemma OAI.TwistedBrin.PartitionMaps.rearrange_chart line 40
  5. def OAI.TwistedBrin.PartitionMaps.pieces line 45
  6. lemma OAI.TwistedBrin.PartitionMaps.pieces_chart line 59
  7. lemma OAI.TwistedBrin.PartitionMaps.ext line 68
  8. def OAI.TwistedBrin.PartitionMaps.piecesHom line 76
  9. lemma OAI.TwistedBrin.PartitionMaps.piecesHom_apply line 87
  10. lemma OAI.TwistedBrin.PartitionMaps.piecesHom_injective line 90
  11. lemma OAI.TwistedBrin.Prefix.grid_of_chart line 104
  12. def OAI.TwistedBrin.Localization.gridIndex line 118
  13. lemma OAI.TwistedBrin.Localization.gridIndex_prefix line 121
  14. def OAI.TwistedBrin.Localization.hom line 124
  15. lemma OAI.TwistedBrin.Localization.chart line 129
  16. lemma OAI.TwistedBrin.Localization.outside line 136
  17. lemma OAI.TwistedBrin.Localization.injective line 150
  18. lemma OAI.TwistedBrin.Prefix.disjoint_of_length line 164
  19. def OAI.TwistedBrin.BrickSwap.fn line 173
  20. lemma OAI.TwistedBrin.BrickSwap.chart_left line 178
  21. lemma OAI.TwistedBrin.BrickSwap.chart_right line 182
  22. lemma OAI.TwistedBrin.BrickSwap.outside line 186
  23. lemma OAI.TwistedBrin.BrickSwap.involutive line 190
  24. def OAI.TwistedBrin.BrickSwap.elem line 200
  25. lemma OAI.TwistedBrin.BrickSwap.elem_apply line 222
  26. lemma OAI.TwistedBrin.BrickSwap.elem_left line 224
  27. lemma OAI.TwistedBrin.BrickSwap.elem_right line 225
  28. lemma OAI.TwistedBrin.BrickSwap.elem_sq line 227
  29. lemma OAI.TwistedBrin.BrickSwap.elem_inv line 231
  30. lemma OAI.TwistedBrin.Localization.apply_mem_iff line 236
  31. lemma OAI.TwistedBrin.Localization.conjugate line 244
  32. lemma OAI.TwistedBrin.Localization.conjugate_swap line 261
  33. lemma OAI.TwistedBrin.Localization.append line 265
  34. lemma OAI.TwistedBrin.Prefix.exists_disjoint line 290
  35. lemma OAI.TwistedBrin.Prefix.cut_partition line 298
  36. lemma OAI.TwistedBrin.Prefix.cut_ne_empty line 304
  37. lemma OAI.TwistedBrin.Prefix.append_ne_empty_left line 309
  38. lemma OAI.TwistedBrin.Prefix.chart_cut_commute line 318
  39. lemma OAI.TwistedBrin.Prefix.mem_cut_chart_iff line 329
  40. lemma OAI.TwistedBrin.Localization.image_eq_of_disjoint line 343
  41. lemma OAI.TwistedBrin.Localization.image_eq_proper line 352
  42. def OAI.TwistedBrin.Stationary line 370
  43. lemma OAI.TwistedBrin.Stationary.split line 374
  44. lemma OAI.TwistedBrin.Stationary.localize line 392
  45. lemma OAI.TwistedBrin.Stationary.local_image_eq_one line 412
  46. lemma OAI.TwistedBrin.Stationary.image_eq_one line 420
  47. lemma OAI.TwistedBrin.PartitionMaps.stationary_rearrange line 426
  48. lemma OAI.TwistedBrin.PartitionMaps.fresh line 434
  49. lemma OAI.TwistedBrin.PartitionMaps.rearrange_image line 448
  50. lemma OAI.TwistedBrin.PartitionMaps.rearrange_local_image line 453
  51. lemma OAI.TwistedBrin.Localization.cuts_chart line 464
  52. lemma OAI.TwistedBrin.Localization.empty line 481
  53. lemma OAI.TwistedBrin.global_split line 488
  54. lemma OAI.TwistedBrin.PerfectProducer.global_local_image line 510
  55. lemma OAI.TwistedBrin.PerfectProducer.global_image line 520
  56. lemma OAI.TwistedBrin.PerfectProducer.global_local_image_all line 526
  57. lemma OAI.TwistedBrin.PartitionMaps.pieces_mulSingle line 534
  58. lemma OAI.TwistedBrin.PerfectProducer.pieces_global_image line 553
  59. lemma OAI.TwistedBrin.PerfectProducer.hom_eq_one line 572
  60. lemma OAI.TwistedBrin.localGroup_perfect line 587