OAI/Topology/ArtinGroups/Coxeter/AmbientCoxeterFace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.restriction_parabolic_image line 14
2. lemma OAI.HarmonicArtin.restriction_word line 28
3. def OAI.HarmonicArtin.ambientCoxeterFace line 32
4. lemma OAI.HarmonicArtin.ambientCoxeterFace_le_iff line 41
5. def OAI.HarmonicArtin.sourceFaceLifted line 60
6. lemma OAI.HarmonicArtin.sourceFaceLifted_le_iff line 65
7. lemma OAI.HarmonicArtin.sourceFaceLifted_full line 105
8. lemma OAI.HarmonicArtin.sourceFaceLifted_surjective line 120
9. def OAI.HarmonicArtin.sourceCellFaceIso line 145