OAI/Topology/ArtinGroups/Coxeter/VertexCoxeterFace.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.sourceFaceMap_labels line 12
2. lemma OAI.HarmonicArtin.coxeterParabolic_empty_eq line 23
3. def OAI.HarmonicArtin.vertexCoxeterFace line 26
4. lemma OAI.HarmonicArtin.vertexCoxeterFace_vertices line 33
5. lemma OAI.HarmonicArtin.face_empty_eq_vertex line 40
6. lemma OAI.HarmonicArtin.faceCenter_vertex line 43
7. lemma OAI.HarmonicArtin.permutahedron_vertex_point line 49
8. lemma OAI.HarmonicArtin.geometricFaceInclusion_vertex_type line 54
9. lemma OAI.HarmonicArtin.sourceModelFaceMap_vertex line 62
10. lemma OAI.HarmonicArtin.sourceModelFaceMap_center line 72