OAI/GroupTheory/SimpleAmenable/PolygonGeometry/AxisAnchorFamily.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.AxisAnchorFamily line 15
  2. theorem OAI.SimpleAmenable.AxisAnchorFamily.intervalLength line 24
  3. theorem OAI.SimpleAmenable.AxisAnchorFamily.atom_le_cell line 30
  4. theorem OAI.SimpleAmenable.AxisAnchorFamily.atom_disjoint line 39
  5. theorem OAI.SimpleAmenable.AxisAnchorFamily.anchorCopy_eq_cell line 60
  6. theorem OAI.SimpleAmenable.AxisAnchorFamily.anchorCopies_commute line 72
  7. theorem OAI.SimpleAmenable.AxisAnchorFamily.atoms_commute line 82
  8. theorem OAI.SimpleAmenable.AxisAnchorFamily.prefixes_central line 102
  9. def OAI.SimpleAmenable.growthOldLength line 132
  10. def OAI.SimpleAmenable.growthNewLength line 134
  11. def OAI.SimpleAmenable.growthAnchorLength line 136
  12. def OAI.SimpleAmenable.growthAnchorStart line 138
  13. theorem OAI.SimpleAmenable.growth_lengths line 140
  14. theorem OAI.SimpleAmenable.growth_anchor_label line 147
  15. def OAI.SimpleAmenable.growthAnchorFamily line 161
  16. theorem OAI.SimpleAmenable.growthAnchorFamily.length line 188
  17. theorem OAI.SimpleAmenable.growthAnchorFamily.start line 191
  18. theorem OAI.SimpleAmenable.growthAnchorFamily.mem line 195
  19. theorem OAI.SimpleAmenable.growthAnchorFamily.range line 201
  20. theorem OAI.SimpleAmenable.growthAnchorFamily.labels line 207
  21. theorem OAI.SimpleAmenable.growthAnchorFamily.label_difference line 217
  22. theorem OAI.SimpleAmenable.growthAnchorFamily.width line 230