OAI/GroupTheory/Thompson/StandardPL.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The ordinary finite-piece dyadic PL condition

A witness is a finite subdivision of the actual real interval, together with an affine equality on each closed piece. Knots may be redundant. The witness is existential in HasDyadicPLPieces, so its choice is not part of a group element's identity.

  1. theorem OAI.ThompsonNonamenability.DyadicPLWitness.knot_le_next line 22
  2. theorem OAI.ThompsonNonamenability.DyadicPLWitness.image_knots_dyadic line 26
  3. theorem OAI.ThompsonNonamenability.DyadicPLWitness.map_dyadic line 37
  4. def OAI.ThompsonNonamenability.DyadicPLWitness.identity line 45
  5. def OAI.ThompsonNonamenability.DyadicPLWitness.inverse line 70
  6. theorem OAI.ThompsonNonamenability.hasDyadicPLPieces_one line 104
  7. theorem OAI.ThompsonNonamenability.HasDyadicPLPieces.inv line 107
  8. theorem OAI.ThompsonNonamenability.HasDyadicPLPieces.map_dyadic line 112
  9. def OAI.ThompsonNonamenability.F.toIntervalHomeomorph line 120
  10. instance OAI.ThompsonNonamenability.F.(instance at line 122) line 122
  11. def OAI.ThompsonNonamenability.F.toHomeomorph line 125
  12. theorem OAI.ThompsonNonamenability.F.strictMono line 128
  13. theorem OAI.ThompsonNonamenability.F.hasDyadicPLPieces line 130
  14. def OAI.ThompsonNonamenability.F.witness line 133
  15. theorem OAI.ThompsonNonamenability.F.map_dyadic line 136
  16. theorem OAI.ThompsonNonamenability.F.map_zero line 140
  17. theorem OAI.ThompsonNonamenability.F.map_one line 143
  18. theorem OAI.ThompsonNonamenability.F.ext line 146