OAI/Combinatorics/Chromatic/QuantumTorus/NearCutGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_convex line 18
2. def OAI.ElementaryPositivity.QuantumTorus.nearCutProbes line 37
3. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_of_probes line 44
4. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_path line 77
5. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_regular_point line 88
6. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_old_negative line 123
7. lemma OAI.ElementaryPositivity.QuantumTorus.nearCut_new_negative line 135