OAI/Combinatorics/Chromatic/Walls/AffineCutTelescoping.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.AffineCut.beforeSideline 9 - def
OAI.ElementaryPositivity.AffineCut.afterSideline 11 - lemma
OAI.ElementaryPositivity.AffineCut.sides_eq_of_neline 14 - lemma
OAI.ElementaryPositivity.AffineCut.sides_at_zeroline 19 - lemma
OAI.ElementaryPositivity.AffineCut.gap_sidesline 24 - theorem
OAI.ElementaryPositivity.AffineCut.telescopeline 68 - lemma
OAI.ElementaryPositivity.AffineCut.sort_strictline 106 - theorem
OAI.ElementaryPositivity.AffineCut.telescope_sortline 110