OAI/GroupTheory/Thompson/IntervalCharts.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual affine charts of basic intervals

The chart is bundled as a point of the real unit interval. Affine transport means equality of these actual maps at every point, including both endpoints.

  1. def OAI.ThompsonNonamenability.BasicInterval.chartPoint line 19
  2. theorem OAI.ThompsonNonamenability.BasicInterval.coe_chartPoint line 23
  3. theorem OAI.ThompsonNonamenability.BasicInterval.chartPoint_injective line 26
  4. theorem OAI.ThompsonNonamenability.BasicInterval.chartPoint_comp line 32
  5. theorem OAI.ThompsonNonamenability.BasicInterval.chartPoint_mem_carrier line 37
  6. theorem OAI.ThompsonNonamenability.BasicInterval.exists_chartPoint line 41
  7. theorem OAI.ThompsonNonamenability.BasicInterval.left_isDyadic line 58
  8. theorem OAI.ThompsonNonamenability.BasicInterval.right_isDyadic line 61
  9. def OAI.ThompsonNonamenability.CarriesAffinely line 67
  10. theorem OAI.ThompsonNonamenability.CarriesAffinely.chartPoint line 72
  11. theorem OAI.ThompsonNonamenability.CarriesAffinely.comp line 76
  12. theorem OAI.ThompsonNonamenability.CarriesAffinely.maps_carrier line 82
  13. theorem OAI.ThompsonNonamenability.CarriesAffinely.preimage_carrier line 88