OAI/GroupTheory/FiniteType/TwistedBrinPatternFactor.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TwistedBrin.Pattern.Factor line 21
  2. def OAI.TwistedBrin.Pattern.Factor.fromLeaf line 27
  3. def OAI.TwistedBrin.Pattern.SplitView.uniformCons line 36
  4. theorem OAI.TwistedBrin.Pattern.uniform_factor_exists line 60
  5. instance OAI.TwistedBrin.Pattern.leavesNonempty line 84
  6. lemma OAI.TwistedBrin.Pattern.Factor.card_le line 88
  7. lemma OAI.TwistedBrin.Pattern.uniform_card line 96
  8. lemma OAI.TwistedBrin.Pattern.mem_coordinates_of_prefix_nonempty line 104
  9. def OAI.TwistedBrin.Pattern.firstCoordinates line 122
  10. lemma OAI.TwistedBrin.Pattern.mem_firstCoordinates line 126
  11. lemma OAI.TwistedBrin.Pattern.firstCoordinates_nonempty line 135
  12. lemma OAI.TwistedBrin.Pattern.firstCoordinates_factor line 141
  13. lemma OAI.TwistedBrin.Pattern.firstCoordinates_card_bound line 148
  14. lemma OAI.TwistedBrin.Pattern.firstCoordinates_uniform line 158
  15. lemma OAI.TwistedBrin.Basis.Forest.cutRefines_factor line 170
  16. def OAI.TwistedBrin.Basis.gridExpansion line 182
  17. lemma OAI.TwistedBrin.Basis.cutRefines_gridExpansion line 185
  18. lemma OAI.TwistedBrin.Basis.rank_gridExpansion line 188
  19. lemma OAI.TwistedBrin.Basis.Forest.gridExpansion_refines line 193
  20. def OAI.TwistedBrin.Basis.Forest.firstGrid line 200
  21. lemma OAI.TwistedBrin.Basis.Forest.firstGrid_lower line 203
  22. lemma OAI.TwistedBrin.Basis.Forest.firstGrid_upper line 206
  23. lemma OAI.TwistedBrin.Pattern.firstCoordinates_eq_of_pieces_eq line 214
  24. lemma OAI.TwistedBrin.Basis.Forest.leaf_restricts line 238
  25. lemma OAI.TwistedBrin.Basis.Forest.pieces_eq line 243
  26. lemma OAI.TwistedBrin.Basis.Forest.firstCoordinates_eq line 261
  27. lemma OAI.TwistedBrin.Basis.Forest.firstGrid_eq line 265
  28. lemma OAI.TwistedBrin.Basis.gridExpansion_mono line 272
  29. lemma OAI.TwistedBrin.Pattern.firstCoordinates_graft line 285
  30. lemma OAI.TwistedBrin.Pattern.firstCoordinates_leaf line 295
  31. lemma OAI.TwistedBrin.Basis.Forest.firstCoordinates_mono line 305
  32. lemma OAI.TwistedBrin.Basis.Forest.firstCoordinates_of_grid_eq line 311
  33. lemma OAI.TwistedBrin.Basis.gridExpansion_injective line 319
  34. lemma OAI.TwistedBrin.Basis.gridExpansion_empty line 326
  35. lemma OAI.TwistedBrin.Basis.Forest.firstGrid_ne line 329
  36. def OAI.TwistedBrin.Basis.firstCuts line 342
  37. lemma OAI.TwistedBrin.Basis.firstCuts_forest line 345
  38. lemma OAI.TwistedBrin.Basis.firstCuts_mono line 349
  39. lemma OAI.TwistedBrin.Basis.firstCuts_grid line 353
  40. lemma OAI.TwistedBrin.Basis.gridExpansion_refines_iff line 358
  41. def OAI.TwistedBrin.Basis.firstCore line 367
  42. lemma OAI.TwistedBrin.Basis.firstCore_lower line 370
  43. lemma OAI.TwistedBrin.Basis.firstCore_upper line 373
  44. lemma OAI.TwistedBrin.Basis.firstCore_ne line 376
  45. lemma OAI.TwistedBrin.Basis.firstCore_mono line 379
  46. lemma OAI.TwistedBrin.Basis.firstCore_grid line 383
  47. structure OAI.TwistedBrin.Basis.CutInterval line 390
  48. lemma OAI.TwistedBrin.Basis.CutInterval.ext line 397
  49. instance OAI.TwistedBrin.Basis.CutInterval.(instance at line 399) line 399
  50. instance OAI.TwistedBrin.Basis.CutInterval.(instance at line 404) line 404
  51. def OAI.TwistedBrin.Basis.CutInterval.core line 412
  52. lemma OAI.TwistedBrin.Basis.CutInterval.core_le line 415
  53. lemma OAI.TwistedBrin.Basis.CutInterval.core_mono line 416
  54. lemma OAI.TwistedBrin.Basis.CutInterval.core_core line 419
  55. def OAI.TwistedBrin.Basis.CutInterval.coreHom line 423
  56. lemma OAI.TwistedBrin.Basis.CutInterval.core_ne_bottom line 426
  57. lemma OAI.TwistedBrin.Basis.CutInterval.core_ne_top line 428
  58. def OAI.TwistedBrin.Basis.CutSelections line 436
  59. instance OAI.TwistedBrin.Basis.CutSelections.(instance at line 441) line 441
  60. def OAI.TwistedBrin.Basis.CutSelections.toInterval line 444
  61. def OAI.TwistedBrin.Basis.CutSelections.ofInterval line 447
  62. lemma OAI.TwistedBrin.Basis.CutSelections.of_to line 450
  63. lemma OAI.TwistedBrin.Basis.CutSelections.to_of line 453
  64. lemma OAI.TwistedBrin.Basis.CutSelections.to_le_iff line 456
  65. lemma OAI.TwistedBrin.Basis.CutSelections.to_mono line 459
  66. lemma OAI.TwistedBrin.Basis.CutSelections.of_mono line 462
  67. def OAI.TwistedBrin.Basis.CutSelections.fixedEquiv line 466