OAI/GroupTheory/ArtinCAT0/Centralizer.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArtinCAT0.GeodesicallyConvex line 11
2. lemma OAI.ArtinCAT0.CAT0_subtype line 15
3. def OAI.ArtinCAT0.tupleCentralizer line 44
4. def OAI.ArtinCAT0.displacementSublevel line 50
5. lemma OAI.ArtinCAT0.displacementSublevel_closed line 53
6. lemma OAI.ArtinCAT0.displacementSublevel_convex line 61
7. lemma OAI.ArtinCAT0.displacementSublevel_smul line 73
8. def OAI.ArtinCAT0.sublevelAction line 83
9. lemma OAI.ArtinCAT0.sublevelAction_isometry line 89
10. lemma OAI.ArtinCAT0.sublevelAction_proper line 97
11. lemma OAI.ArtinCAT0.sublevelAction_cocompact line 113
12. theorem OAI.ArtinCAT0.geometric_tupleCentralizer line 169

    Source documentation

    The finite-tuple geometric centralizer theorem, with no commutation hypothesis on the tuple itself and no dimension hypothesis.

    theorem geometric_tupleCentralizer [Finite ι] [ProperSpace X] [Nonempty X]
        (hG : GeometricAction G X) (q : ι → G) (A : ℝ) (hA : 0 ≤ A) :
        letI := sublevelAction hG.2.1 q A
    …

    Mentions: OAI.ArtinCAT0.sublevelAction

13. lemma OAI.ArtinCAT0.sublevelAction_stableLength line 178
14. lemma OAI.ArtinCAT0.exists_sublevel_nonempty line 185
15. lemma OAI.ArtinCAT0.sublevel_properSpace line 194