OAI/GroupTheory/Thompson/BasicInterval.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Basic dyadic intervals

A cell records its actual depth and its index on that dyadic grid. Its endpoints determine the record uniquely. Composition is the affine image of one cell inside another; no formal interval identifications are assumed.

  1. structure OAI.ThompsonNonamenability.BasicInterval line 22
  2. theorem OAI.ThompsonNonamenability.BasicInterval.ext_depth_index line 29
  3. def OAI.ThompsonNonamenability.BasicInterval.left line 41
  4. def OAI.ThompsonNonamenability.BasicInterval.right line 43
  5. def OAI.ThompsonNonamenability.BasicInterval.length line 45
  6. def OAI.ThompsonNonamenability.BasicInterval.carrier line 47
  7. def OAI.ThompsonNonamenability.BasicInterval.interior line 49
  8. def OAI.ThompsonNonamenability.BasicInterval.Internal line 51
  9. def OAI.ThompsonNonamenability.BasicInterval.Before line 53
  10. def OAI.ThompsonNonamenability.BasicInterval.Contained line 55
  11. def OAI.ThompsonNonamenability.BasicInterval.chart line 57
  12. theorem OAI.ThompsonNonamenability.BasicInterval.denominator_pos line 60
  13. theorem OAI.ThompsonNonamenability.BasicInterval.denominator_ne_zero line 63
  14. theorem OAI.ThompsonNonamenability.BasicInterval.length_pos line 66
  15. theorem OAI.ThompsonNonamenability.BasicInterval.length_eq_right_sub_left line 69
  16. theorem OAI.ThompsonNonamenability.BasicInterval.left_nonneg line 74
  17. theorem OAI.ThompsonNonamenability.BasicInterval.right_le_one line 77
  18. theorem OAI.ThompsonNonamenability.BasicInterval.left_lt_right line 81
  19. theorem OAI.ThompsonNonamenability.BasicInterval.carrier_subset_unit line 85
  20. theorem OAI.ThompsonNonamenability.BasicInterval.interior_subset_carrier line 89
  21. theorem OAI.ThompsonNonamenability.BasicInterval.interior_nonempty line 93
  22. theorem OAI.ThompsonNonamenability.BasicInterval.contained_refl line 97
  23. theorem OAI.ThompsonNonamenability.BasicInterval.Contained.trans line 99
  24. theorem OAI.ThompsonNonamenability.BasicInterval.Contained.carrier_subset line 103
  25. theorem OAI.ThompsonNonamenability.BasicInterval.Contained.interior_subset line 108
  26. theorem OAI.ThompsonNonamenability.BasicInterval.length_le_of_contained line 113
  27. theorem OAI.ThompsonNonamenability.BasicInterval.chart_zero line 118
  28. theorem OAI.ThompsonNonamenability.BasicInterval.chart_one line 121
  29. theorem OAI.ThompsonNonamenability.BasicInterval.chart_eq_left_add_length_mul line 123
  30. theorem OAI.ThompsonNonamenability.BasicInterval.chart_strictMono line 128
  31. theorem OAI.ThompsonNonamenability.BasicInterval.chart_injective line 133
  32. theorem OAI.ThompsonNonamenability.BasicInterval.chart_mem_self_carrier_iff line 136
  33. theorem OAI.ThompsonNonamenability.BasicInterval.chart_mem_self_interior_iff line 142
  34. theorem OAI.ThompsonNonamenability.BasicInterval.ext_endpoints line 148
  35. def OAI.ThompsonNonamenability.BasicInterval.root line 163
  36. theorem OAI.ThompsonNonamenability.BasicInterval.root_depth line 165
  37. theorem OAI.ThompsonNonamenability.BasicInterval.root_index line 167
  38. theorem OAI.ThompsonNonamenability.BasicInterval.root_left line 169
  39. theorem OAI.ThompsonNonamenability.BasicInterval.root_right line 171
  40. theorem OAI.ThompsonNonamenability.BasicInterval.root_length line 173
  41. theorem OAI.ThompsonNonamenability.BasicInterval.root_chart line 175
  42. def OAI.ThompsonNonamenability.BasicInterval.comp line 177
  43. theorem OAI.ThompsonNonamenability.BasicInterval.comp_depth line 188
  44. theorem OAI.ThompsonNonamenability.BasicInterval.comp_index line 190
  45. theorem OAI.ThompsonNonamenability.BasicInterval.chart_comp line 193
  46. theorem OAI.ThompsonNonamenability.BasicInterval.left_comp line 200
  47. theorem OAI.ThompsonNonamenability.BasicInterval.right_comp line 203
  48. theorem OAI.ThompsonNonamenability.BasicInterval.comp_assoc line 206
  49. theorem OAI.ThompsonNonamenability.BasicInterval.comp_root line 212
  50. theorem OAI.ThompsonNonamenability.BasicInterval.root_comp line 215
  51. theorem OAI.ThompsonNonamenability.BasicInterval.comp_left_injective line 218
  52. theorem OAI.ThompsonNonamenability.BasicInterval.comp_injective line 226
  53. theorem OAI.ThompsonNonamenability.BasicInterval.comp_contained line 229
  54. theorem OAI.ThompsonNonamenability.BasicInterval.chart_mem_carrier_iff line 236
  55. theorem OAI.ThompsonNonamenability.BasicInterval.chart_mem_interior_iff line 240
  56. theorem OAI.ThompsonNonamenability.BasicInterval.comp_contained_iff line 244
  57. theorem OAI.ThompsonNonamenability.BasicInterval.comp_internal_of_internal_right line 248
  58. theorem OAI.ThompsonNonamenability.BasicInterval.comp_internal line 260
  59. theorem OAI.ThompsonNonamenability.BasicInterval.comp_before_comp line 263