OAI/GroupTheory/FiniteType/TwistedBrinRangeChartRestricts.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TwistedBrin.GermBrick.range_chart_restricts line 21
  2. def OAI.TwistedBrin.Basis.ofPartition line 34
  3. lemma OAI.TwistedBrin.Basis.mem_ofPartition line 52
  4. lemma OAI.TwistedBrin.Basis.exists_prefix_of_mem_ofPartition line 58
  5. def OAI.TwistedBrin.Basis.grid line 65
  6. lemma OAI.TwistedBrin.Basis.grid_refines_grid line 68
  7. lemma OAI.TwistedBrin.Basis.local_standard_refinement line 80
  8. lemma OAI.TwistedBrin.Basis.has_grid_refinement line 95
  9. lemma OAI.TwistedBrin.Basis.directed line 115
  10. lemma OAI.TwistedBrin.Prefix.eq_empty_of_brick_univ line 131
  11. lemma OAI.TwistedBrin.GermBrick.eq_of_restricts_of_region_eq line 148
  12. lemma OAI.TwistedBrin.Basis.ext line 164
  13. lemma OAI.TwistedBrin.Basis.eq_of_common_point line 168
  14. lemma OAI.TwistedBrin.Basis.refines_ancestor_unique line 172
  15. lemma OAI.TwistedBrin.Basis.pieces_subset_of_refines_both line 178
  16. lemma OAI.TwistedBrin.Basis.refines_antisymm line 193
  17. instance OAI.TwistedBrin.Basis.(instance at line 197) line 197
  18. lemma OAI.TwistedBrin.Basis.le_def line 203
  19. def OAI.TwistedBrin.Basis.ancestor line 205
  20. lemma OAI.TwistedBrin.Basis.ancestor_restricts line 206
  21. lemma OAI.TwistedBrin.Basis.ancestor_surjective line 209
  22. lemma OAI.TwistedBrin.Basis.rank_eq_card line 217
  23. lemma OAI.TwistedBrin.Basis.rank_mono line 220
  24. lemma OAI.TwistedBrin.Basis.translate_one line 224
  25. lemma OAI.TwistedBrin.Basis.translate_mul line 231
  26. instance OAI.TwistedBrin.Basis.(instance at line 242) line 242
  27. lemma OAI.TwistedBrin.Basis.translate_mono line 247
  28. lemma OAI.TwistedBrin.Basis.eq_of_le_of_rank_eq line 256
  29. lemma OAI.TwistedBrin.Basis.rank_strictMono line 277
  30. lemma OAI.TwistedBrin.locallyStandard_of_charts line 285
  31. def OAI.TwistedBrin.Basis.transition line 317
  32. lemma OAI.TwistedBrin.Basis.transition_chart line 320
  33. lemma OAI.TwistedBrin.Basis.transition_isLocal line 327
  34. def OAI.TwistedBrin.Basis.transitionElement line 334
  35. lemma OAI.TwistedBrin.Basis.transition_germBrick line 337
  36. lemma OAI.TwistedBrin.Basis.translate_transition line 345
  37. lemma OAI.TwistedBrin.Basis.orbit_of_rank_eq line 362
  38. lemma OAI.TwistedBrin.twist_injective line 373
  39. def OAI.TwistedBrin.Basis.twistPieces line 389
  40. lemma OAI.TwistedBrin.Basis.twistPieces_chart line 393
  41. lemma OAI.TwistedBrin.Basis.twistPieces_isLocal line 400
  42. def OAI.TwistedBrin.Basis.twistPiecesHom line 408
  43. lemma OAI.TwistedBrin.Basis.twistPiecesHom_injective line 428
  44. def OAI.TwistedBrin.Basis.rigidStabilizer line 440
  45. lemma OAI.TwistedBrin.Basis.twistPiecesHom_mem_rigidStabilizer line 460
  46. lemma OAI.TwistedBrin.Basis.exists_chart_twist_of_mem_rigidStabilizer line 470
  47. lemma OAI.TwistedBrin.Basis.exists_twistPiecesHom_of_mem line 479
  48. def OAI.TwistedBrin.Basis.rigidStabilizerEquiv line 490