OAI/Topology/ArtinGroups/Harmonic/SphericalLongest.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.parabolic_longest_unique line 16
2. def OAI.HarmonicArtin.sphericalLongest line 24
3. lemma OAI.HarmonicArtin.sphericalLongest_spec line 27
4. lemma OAI.HarmonicArtin.positiveToArtin_simpleLift line 32
5. def OAI.HarmonicArtin.liftedTopVertex line 36
6. def OAI.HarmonicArtin.cellWithTop line 39
7. lemma OAI.HarmonicArtin.cellWithTop_top line 42
8. lemma OAI.HarmonicArtin.cellWithTop_topVertex line 46
9. lemma OAI.HarmonicArtin.cellWithTop_mono line 51
10. abbrev OAI.HarmonicArtin.PositiveTopBlock line 56
11. instance OAI.HarmonicArtin.(instance at line 60) line 60
12. theorem OAI.HarmonicArtin.positiveTopBlock_has_greatest line 64
13. theorem OAI.HarmonicArtin.positiveTopBlock_contractible line 100
14. theorem OAI.HarmonicArtin.spherical_positiveTopBlock_contractible line 113