OAI/GroupTheory/FiniteType/TwistedBrinBasis.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TwistedBrin.Basis.vertexStabilizer line 20
  2. lemma OAI.TwistedBrin.Basis.rigid_le_vertexStabilizer line 23
  3. lemma OAI.TwistedBrin.Basis.vertex_mem_iff line 39
  4. def OAI.TwistedBrin.Basis.vertexPermutationHom line 53
  5. lemma OAI.TwistedBrin.Basis.vertexPermutationHom_apply line 67
  6. lemma OAI.TwistedBrin.Basis.mem_vertexPermutationHom_ker line 70
  7. def OAI.TwistedBrin.Basis.twistPiecesToVertex line 81
  8. def OAI.TwistedBrin.Basis.twistPiecesToKernel line 85
  9. def OAI.TwistedBrin.Basis.vertexKernelEquiv line 89
  10. instance OAI.TwistedBrin.Basis.vertexPermutationHom_ker_finiteIndex line 98
  11. def OAI.TwistedBrin.Prefix.cut line 109
  12. lemma OAI.TwistedBrin.Prefix.cut_apply line 117
  13. lemma OAI.TwistedBrin.Prefix.mem_cut_iff line 121
  14. lemma OAI.TwistedBrin.Prefix.mem_append_iff line 137
  15. inductive OAI.TwistedBrin.Pattern line 151
  16. def OAI.TwistedBrin.Pattern.Leaves line 158
  17. instance OAI.TwistedBrin.Pattern.leavesFintype line 162
  18. def OAI.TwistedBrin.Pattern.leafPrefix line 169
  19. lemma OAI.TwistedBrin.Pattern.split_prefix_nonempty line 174
  20. lemma OAI.TwistedBrin.Pattern.partition line 181
  21. lemma OAI.TwistedBrin.Pattern.leafPrefix_injective line 212
  22. def OAI.TwistedBrin.Pattern.pieces line 219
  23. lemma OAI.TwistedBrin.Pattern.mem_pieces line 223
  24. lemma OAI.TwistedBrin.Pattern.pieces_split_nonempty line 227
  25. def OAI.TwistedBrin.UnslicedPartition.data line 237
  26. lemma OAI.TwistedBrin.UnslicedPartition.boolean_partition line 242
  27. lemma OAI.TwistedBrin.UnslicedPartition.missing_coordinate line 247
  28. lemma OAI.TwistedBrin.UnslicedPartition.data_injective line 248
  29. def OAI.TwistedBrin.UnslicedPartition.tile line 250
  30. lemma OAI.TwistedBrin.UnslicedPartition.mem_tile_iff line 254
  31. lemma OAI.TwistedBrin.UnslicedPartition.tile_partition line 274
  32. def OAI.TwistedBrin.UnslicedPartition.pieces line 279
  33. lemma OAI.TwistedBrin.UnslicedPartition.all_tiles_mem line 283
  34. lemma OAI.TwistedBrin.UnslicedPartition.tile_injective line 287
  35. lemma OAI.TwistedBrin.UnslicedPartition.card_pieces line 295
  36. lemma OAI.TwistedBrin.UnslicedPartition.no_binary_pattern line 300
  37. def OAI.TwistedBrin.Prefix.inflate line 324
  38. lemma OAI.TwistedBrin.Prefix.inflate_apply line 333
  39. lemma OAI.TwistedBrin.Prefix.inflate_injective line 336
  40. lemma OAI.TwistedBrin.Prefix.mem_inflate_iff line 343
  41. def OAI.TwistedBrin.UnslicedPartition.infiniteTile line 362
  42. lemma OAI.TwistedBrin.UnslicedPartition.infiniteTile_partition line 364
  43. lemma OAI.TwistedBrin.UnslicedPartition.infiniteTile_injective line 369
  44. lemma OAI.TwistedBrin.UnslicedPartition.infiniteTile_missing line 372
  45. def OAI.TwistedBrin.UnslicedPartition.infinitePieces line 382
  46. lemma OAI.TwistedBrin.UnslicedPartition.infiniteTile_mem line 386
  47. lemma OAI.TwistedBrin.UnslicedPartition.card_infinitePieces line 390
  48. lemma OAI.TwistedBrin.UnslicedPartition.no_binary_pattern_infinite line 395
  49. def OAI.TwistedBrin.UnslicedPartition.basis line 413
  50. lemma OAI.TwistedBrin.UnslicedPartition.trivial_le_basis line 415
  51. def OAI.TwistedBrin.Basis.ofChartPartition line 429
  52. lemma OAI.TwistedBrin.Basis.chartPartition_injective line 447
  53. lemma OAI.TwistedBrin.Basis.rank_ofChartPartition line 459
  54. def OAI.TwistedBrin.Basis.expandedChart line 467
  55. lemma OAI.TwistedBrin.Basis.expanded_partition line 472
  56. def OAI.TwistedBrin.Basis.expand line 498
  57. lemma OAI.TwistedBrin.Basis.rank_expand line 501
  58. lemma OAI.TwistedBrin.Basis.refines_expand line 505
  59. lemma OAI.TwistedBrin.Basis.expand_leaf line 512