OAI/GroupTheory/FiniteType/TwistedBrinPattern.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TwistedBrin.Pattern.Pruning line 20
  2. lemma OAI.TwistedBrin.Pattern.pruning_exists line 32
  3. lemma OAI.TwistedBrin.Basis.Forest.eq_of_all_leaf line 107
  4. def OAI.TwistedBrin.Basis.Forest.prunedMerge line 119
  5. lemma OAI.TwistedBrin.Basis.Forest.cutRefines_pruned line 136
  6. lemma OAI.TwistedBrin.Basis.Forest.exists_last_merge line 177
  7. abbrev OAI.TwistedBrin.Basis.Descending line 194
  8. def OAI.TwistedBrin.Basis.DownAdjacent line 196
  9. abbrev OAI.TwistedBrin.Basis.DownConnected line 199
  10. def OAI.TwistedBrin.Basis.Merge.vertex line 205
  11. lemma OAI.TwistedBrin.Basis.Merge.connected_of_disjoint line 208
  12. lemma OAI.TwistedBrin.Basis.Merge.exists_disjoint_pair line 220
  13. lemma OAI.TwistedBrin.Basis.Merge.connected line 246
  14. lemma OAI.TwistedBrin.Basis.descending_connected line 253
  15. lemma OAI.TwistedBrin.Oligomorphic.finite_palette line 265
  16. def OAI.TwistedBrin.Pattern.nodes line 284
  17. def OAI.TwistedBrin.Pattern.depth line 288
  18. def OAI.TwistedBrin.Pattern.coordinates line 292
  19. lemma OAI.TwistedBrin.Pattern.nodes_add_one line 296
  20. lemma OAI.TwistedBrin.Pattern.depth_le_nodes line 304
  21. lemma OAI.TwistedBrin.Pattern.coordinates_card_le line 309
  22. lemma OAI.TwistedBrin.Pattern.coordinates_relabel line 319
  23. lemma OAI.TwistedBrin.Pattern.depth_relabel line 326
  24. def OAI.TwistedBrin.Pattern.bounded line 332
  25. lemma OAI.TwistedBrin.Pattern.mem_bounded line 339
  26. lemma OAI.TwistedBrin.Pattern.finite_orbit_representatives line 359
  27. lemma OAI.TwistedBrin.Basis.twistPieces_expanded_germ line 378
  28. lemma OAI.TwistedBrin.Basis.translate_twistPieces_expand line 393
  29. lemma OAI.TwistedBrin.Basis.Forest.expand_eq line 410
  30. lemma OAI.TwistedBrin.Basis.Forest.leaves_le_rank line 424
  31. lemma OAI.TwistedBrin.Basis.outgoing_finite_orbit_representatives line 432
  32. lemma OAI.TwistedBrin.Prefix.length_le_of_brick_subset line 451
  33. lemma OAI.TwistedBrin.Prefix.brick_injective line 462