OAI/Topology/ArtinGroups/Realizations/RestrictedLiftedCell.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.restriction_parabolic_map line 15
2. lemma OAI.HarmonicArtin.restriction_wordCoxeter line 29
3. def OAI.HarmonicArtin.restrictedLiftedCell line 34
4. lemma OAI.HarmonicArtin.restrictedLiftedCell_injective line 41
5. lemma OAI.HarmonicArtin.restrictedLiftedCell_surjective line 53
6. lemma OAI.HarmonicArtin.restrictedLiftedCell_face_iff line 74
7. def OAI.HarmonicArtin.restrictedLiftedFiberIso line 128