OAI/Topology/ArtinGroups/Harmonic/PredAboveSuccSucc.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.predAbove_succ_succAboveline 13 - lemma
OAI.HarmonicArtin.prismGrid_face_rightline 19 - lemma
OAI.HarmonicArtin.prismGrid_face_adjacentline 31 - lemma
OAI.HarmonicArtin.prismMarginals_face_rightline 40 - lemma
OAI.HarmonicArtin.prismMarginals_face_adjacentline 60 - lemma
OAI.HarmonicArtin.prismPrefix_stepline 80 - lemma
OAI.HarmonicArtin.prismSimplex_face_rightline 89 - lemma
OAI.HarmonicArtin.prismSimplex_face_adjacentline 98 - lemma
OAI.HarmonicArtin.nervePrism_face_adjacentline 108