OAI/GroupTheory/Thompson/AffinePiece.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Affine maps between basic dyadic intervals

Each pair of basic intervals determines an increasing affine map of the real line. It carries endpoints and charts to their counterparts, and its slope is an integral power of two.

  1. def OAI.ThompsonNonamenability.OrderedPLInterpolation.affine line 19
  2. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_left line 22
  3. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_right line 26
  4. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_strictMono line 34
  5. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_inverse line 40
  6. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_chart line 46
  7. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.affine_slope_zpow line 53