OAI/GroupTheory/FiniteType/TwistedBrinPrefix.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TwistedBrin.Prefix.permute_empty line 19
  2. lemma OAI.TwistedBrin.Prefix.permute_append line 20
  3. lemma OAI.TwistedBrin.Prefix.permute_cut line 22
  4. def OAI.TwistedBrin.Pattern.relabel line 35
  5. def OAI.TwistedBrin.Pattern.relabelLeaves line 39
  6. lemma OAI.TwistedBrin.Pattern.relabel_prefix line 43
  7. def OAI.TwistedBrin.Pattern.graft line 58
  8. def OAI.TwistedBrin.Pattern.graftLeaves line 63
  9. lemma OAI.TwistedBrin.Pattern.graft_prefix line 96
  10. structure OAI.TwistedBrin.Basis.Forest line 118
  11. abbrev OAI.TwistedBrin.Basis.Forest.Index line 126
  12. lemma OAI.TwistedBrin.Basis.Forest.refines line 128
  13. def OAI.TwistedBrin.Basis.Forest.refl line 134
  14. def OAI.TwistedBrin.Basis.Forest.expansion line 147
  15. lemma OAI.TwistedBrin.Basis.Forest.exists_gauge line 160
  16. def OAI.TwistedBrin.Basis.Forest.gauge line 168
  17. lemma OAI.TwistedBrin.Basis.Forest.gauge_spec line 171
  18. def OAI.TwistedBrin.Basis.Forest.compositePattern line 176
  19. def OAI.TwistedBrin.Basis.Forest.compositeIndex line 181
  20. lemma OAI.TwistedBrin.Basis.Forest.composite_chart line 191
  21. def OAI.TwistedBrin.Basis.Forest.trans line 208
  22. def OAI.TwistedBrin.Basis.CutRefines line 223
  23. lemma OAI.TwistedBrin.Basis.cutRefines_refl line 225
  24. lemma OAI.TwistedBrin.Basis.cutRefines_trans line 226
  25. lemma OAI.TwistedBrin.Basis.cutRefines_antisymm line 231
  26. lemma OAI.TwistedBrin.Basis.le_of_cutRefines line 233
  27. def OAI.TwistedBrin.Pattern.uniform line 241
  28. lemma OAI.TwistedBrin.Pattern.uniform_length line 245
  29. def OAI.TwistedBrin.Pattern.rectangular line 264
  30. lemma OAI.TwistedBrin.Pattern.rectangular_length line 267
  31. lemma OAI.TwistedBrin.Prefix.eq_of_mem_of_length_eq line 279
  32. lemma OAI.TwistedBrin.Prefix.eq_gridPrefix_of_lengths line 285
  33. lemma OAI.TwistedBrin.Pattern.rectangular_prefix line 294
  34. lemma OAI.TwistedBrin.Pattern.exists_rectangular_leaf line 299
  35. lemma OAI.TwistedBrin.Pattern.rectangular_pieces line 306
  36. lemma OAI.TwistedBrin.LocalEmbedding.rectangular_standard line 324
  37. def OAI.TwistedBrin.Basis.Forest.of_mem line 360
  38. lemma OAI.TwistedBrin.Basis.exists_standard_cut_patterns line 380
  39. lemma OAI.TwistedBrin.Basis.cutRefines_grid_from_patterns line 387
  40. lemma OAI.TwistedBrin.Basis.has_cut_grid_refinement line 429
  41. lemma OAI.TwistedBrin.Basis.cut_grid_cofinal line 445
  42. theorem OAI.TwistedBrin.Basis.cut_directed line 456