OAI/GroupTheory/Thompson/StandardF.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThompsonNonamenability.standardSubgroup line 7
2. instance OAI.ThompsonNonamenability.F.(instance at line 17) line 17
3. theorem OAI.ThompsonNonamenability.F.one_apply line 19
4. theorem OAI.ThompsonNonamenability.F.mul_apply line 21
5. theorem OAI.ThompsonNonamenability.F.inv_apply_apply line 23
6. theorem OAI.ThompsonNonamenability.F.apply_inv_apply line 26
7. def OAI.ThompsonNonamenability.F.toIntervalHomeomorphHom line 29
8. theorem OAI.ThompsonNonamenability.F.toIntervalHomeomorph_injective line 34
9. theorem OAI.ThompsonNonamenability.F.toHomeomorph_injective line 37
10. def OAI.ThompsonNonamenability.F.standardHomeomorphEquiv line 45

    Source documentation

    The representation forgets no mathematical data: it is equivalent to the usual subtype of actual increasing finite dyadic PL interval homeomorphisms.

    def standardHomeomorphEquiv :
        F ≃ {f : UnitInterval ≃ₜ UnitInterval //
          StrictMono f ∧ HasDyadicPLPieces ⟨f⟩} where
    …

    Mentions: OAI.ThompsonNonamenability.F, OAI.ThompsonNonamenability.UnitInterval, OAI.ThompsonNonamenability.HasDyadicPLPieces

11. theorem OAI.ThompsonNonamenability.F.mem_iff_standardPL line 58