OAI/GroupTheory/Thompson/OrderedPLInterpolation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual interpolation of ordered dyadic partitions

Matched cells determine affine maps. They are glued at their common endpoints, and the reverse matching is their inverse. Restricting the resulting real order isomorphism gives the literal interval homeomorphism.

  1. def OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap line 23
  2. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_start line 29
  3. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_eq_tail line 49
  4. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_end line 60
  5. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_strictMono line 75
  6. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_inverse line 108
  7. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_on_cells_aux line 135
  8. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.chainMap_on_cells line 161
  9. def OAI.ThompsonNonamenability.OrderedPLInterpolation.chainOrderIso line 167
  10. def OAI.ThompsonNonamenability.OrderedPLInterpolation.intervalOrderIso line 176
  11. def OAI.ThompsonNonamenability.OrderedPLInterpolation.intervalHomeomorph line 193
  12. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.intervalHomeomorph_strictMono line 197
  13. def OAI.ThompsonNonamenability.OrderedPLInterpolation.interpolationWitness line 202
  14. def OAI.ThompsonNonamenability.OrderedPLInterpolation.transport line 236
  15. theorem OAI.ThompsonNonamenability.OrderedPLInterpolation.transport_on_cells line 241
  16. theorem OAI.ThompsonNonamenability.exists_chain_transport line 252