OAI/GroupTheory/Thompson/Model.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ThompsonNonamenability.UnitInterval line 16

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:16 (same declaration text).

2. def OAI.ThompsonNonamenability.unitIntervalZero line 18

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:18 (same declaration text).

3. def OAI.ThompsonNonamenability.unitIntervalOne line 19

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:19 (same declaration text).

4. structure OAI.ThompsonNonamenability.IntervalHomeomorph line 21

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:21 (same declaration text).

5. instance OAI.ThompsonNonamenability.IntervalHomeomorph.(instance at line 26) line 26
6. def OAI.ThompsonNonamenability.IsDyadic line 31

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:31 (same declaration text).

7. structure OAI.ThompsonNonamenability.DyadicPLWitness line 34

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:34 (same declaration text).

8. def OAI.ThompsonNonamenability.HasDyadicPLPieces line 50

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:50 (same declaration text).

9. def OAI.ThompsonNonamenability.F line 52

   Also declared: ComparatorChallenges/ThompsonNonamenability.lean:52 (same declaration text).

10. abbrev OAI.ThompsonNonamenability.BoundedReal line 54

    Also declared: ComparatorChallenges/ThompsonNonamenability.lean:54 (same declaration text).

11. def OAI.ThompsonNonamenability.leftPull line 58

    Also declared: ComparatorChallenges/ThompsonNonamenability.lean:58 (same declaration text).

12. structure OAI.ThompsonNonamenability.InvariantMean line 71

    Also declared: ComparatorChallenges/ThompsonNonamenability.lean:71 (same declaration text).