OAI/Topology/ArtinGroups/Realizations/PositiveLiftedCell.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.positiveSimpleLift_prefix_longestline 12 - abbrev
OAI.HarmonicArtin.PositiveLiftedCellline 27 - def
OAI.HarmonicArtin.positiveCellToLiftedline 29 - def
OAI.HarmonicArtin.positiveCellTopline 32 - lemma
OAI.HarmonicArtin.positiveCellTop_toArtinline 35 - theorem
OAI.HarmonicArtin.positiveCellTop_prefix_of_faceline 39 - lemma
OAI.HarmonicArtin.positiveCellTop_degree_monoline 67 - lemma
OAI.HarmonicArtin.positiveCellTop_degree_strictline 73