OAI/Topology/ArtinGroups/Harmonic/TypedRightCoset.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.typedRightCoset line 12
2. lemma OAI.HarmonicArtin.cellToDeligne_le_typedRightCoset line 15
3. def OAI.HarmonicArtin.liftedLowerFiberIso line 37
4. lemma OAI.HarmonicArtin.deligne_same_type_eq line 48
5. lemma OAI.HarmonicArtin.deligne_type_strict line 64
6. lemma OAI.HarmonicArtin.deligne_card_strict line 67
7. theorem OAI.HarmonicArtin.salvetti_cover_contractible_of_spherical_fibers line 71