OAI/Combinatorics/Chromatic/Walls/NonpJoint.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ElementaryPositivity.QuantumTorus.nonpSupportFrameline 14 - lemma
OAI.ElementaryPositivity.QuantumTorus.nonpSupportFrame_targetline 31 - lemma
OAI.ElementaryPositivity.QuantumTorus.completedListProduct_congr_throughline 38 - lemma
OAI.ElementaryPositivity.QuantumTorus.planar_joint_supportline 46