OAI/GroupTheory/Thompson/IntervalHomeomorph.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Actual homeomorphisms of the real unit interval

The wrapper supplies the composition group explicitly. In particular, its multiplication is function composition in the order (h * g) x = h (g x). Its carrier is equivalent to the actual interval homeomorphisms, without quotients or an abstract group action.

  1. theorem OAI.ThompsonNonamenability.coe_unitIntervalZero line 19
  2. theorem OAI.ThompsonNonamenability.coe_unitIntervalOne line 20
  3. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.ext line 24
  4. def OAI.ThompsonNonamenability.IntervalHomeomorph.homeomorphEquiv line 32
  5. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.homeomorphEquiv_apply line 38
  6. instance OAI.ThompsonNonamenability.IntervalHomeomorph.(instance at line 41) line 41
  7. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.one_apply line 50
  8. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.mul_apply line 52
  9. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.inv_apply_apply line 55
  10. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.apply_inv_apply line 58
  11. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.injective line 61
  12. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.surjective line 64
  13. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.continuous line 67
  14. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.strictMono_inv line 70
  15. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.map_zero line 79
  16. theorem OAI.ThompsonNonamenability.IntervalHomeomorph.map_one line 89
  17. def OAI.ThompsonNonamenability.IntervalHomeomorph.increasingSubgroup line 99