OAI/GroupTheory/FiniteType/TwistedBrinGermBrick.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TwistedBrin.GermBrick.restricts_iff_chart line 20
  2. lemma OAI.TwistedBrin.GermBrick.eq_of_common_restriction_of_region_eq line 31
  3. def OAI.TwistedBrin.Basis.descendants line 48
  4. lemma OAI.TwistedBrin.Basis.mem_descendants line 52
  5. lemma OAI.TwistedBrin.Basis.region_iff_descendants line 57
  6. lemma OAI.TwistedBrin.Basis.region_eq_of_descendants_eq line 71
  7. lemma OAI.TwistedBrin.Basis.germ_eq_of_region_eq_above line 77
  8. def OAI.TwistedBrin.Basis.intervalCode line 88
  9. lemma OAI.TwistedBrin.Basis.intervalCode_injective line 92
  10. theorem OAI.TwistedBrin.Basis.finite_interval line 114
  11. def OAI.TwistedBrin.Basis.rankModel line 121
  12. lemma OAI.TwistedBrin.Basis.rank_rankModel line 125
  13. lemma OAI.TwistedBrin.Basis.rank_finite_orbit_representatives line 130
  14. lemma OAI.TwistedBrin.Basis.twistPieces_translate_self line 139
  15. lemma OAI.TwistedBrin.Basis.pair_finite_orbit_representatives line 144
  16. lemma OAI.TwistedBrin.Prefix.append_left_cancel line 166
  17. lemma OAI.TwistedBrin.Pattern.root_fixed_of_prefixes_fixed line 177
  18. lemma OAI.TwistedBrin.Pattern.coordinate_rigidity line 196
  19. lemma OAI.TwistedBrin.GermBrick.restriction_injective line 240
  20. def OAI.TwistedBrin.pointwiseStabilizer line 253
  21. lemma OAI.TwistedBrin.Basis.twistPieces_expanded_fixed_iff line 266
  22. lemma OAI.TwistedBrin.Basis.Forest.twistPieces_mem_rigid_iff line 280
  23. def OAI.TwistedBrin.Basis.Forest.rigidPairHom line 296
  24. def OAI.TwistedBrin.Basis.Forest.rigidPairEquiv line 309
  25. def OAI.TwistedBrin.Basis.pairStabilizer line 329
  26. def OAI.TwistedBrin.Basis.pairPermutationHom line 332
  27. lemma OAI.TwistedBrin.Basis.mem_pairPermutationHom_ker line 339
  28. def OAI.TwistedBrin.Basis.rigidPairToKernel line 348
  29. def OAI.TwistedBrin.Basis.rigidPairKernelEquiv line 357
  30. instance OAI.TwistedBrin.Basis.pairPermutationHom_ker_finiteIndex line 366
  31. def OAI.TwistedBrin.Basis.Forest.pairKernelEquiv line 371
  32. def OAI.TwistedBrin.Basis.groupEquiv line 377
  33. def OAI.TwistedBrin.Basis.translateSet line 383
  34. def OAI.TwistedBrin.Basis.intervalSets line 386
  35. lemma OAI.TwistedBrin.Basis.mem_intervalSets_iff line 393
  36. lemma OAI.TwistedBrin.Basis.interval_sets_finite_orbit_representatives line 405
  37. lemma OAI.TwistedBrin.Prefix.cut_append_cut line 425
  38. lemma OAI.TwistedBrin.Prefix.cut_append_commute line 438
  39. structure OAI.TwistedBrin.Pattern.SplitView line 448
  40. def OAI.TwistedBrin.Pattern.shuffle line 454
  41. def OAI.TwistedBrin.Pattern.SplitView.commute line 468
  42. theorem OAI.TwistedBrin.Pattern.splitView_exists line 488