OAI/Combinatorics/Chromatic/Walls/ComparisonLine.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ElementaryPositivity.QuantumTorus.LineRayData line 15
2. lemma OAI.ElementaryPositivity.QuantumTorus.lineRayData_nonempty line 27
3. def OAI.ElementaryPositivity.QuantumTorus.lineRayData line 35
4. lemma OAI.ElementaryPositivity.QuantumTorus.cutSide_decide line 41
5. def OAI.ElementaryPositivity.RationalFiber.actualLineLetter line 64
6. lemma OAI.ElementaryPositivity.RationalFiber.line_cut_event line 86
7. lemma OAI.ElementaryPositivity.RationalFiber.actualLineLetter_high line 92
8. lemma OAI.ElementaryPositivity.QuantumTorus.sort_filter_subset line 117
9. def OAI.ElementaryPositivity.QuantumTorus.intervalLineEvents line 129
10. lemma OAI.ElementaryPositivity.QuantumTorus.intervalLineEvents_mono line 132
11. def OAI.ElementaryPositivity.QuantumTorus.intervalEventList line 139
12. lemma OAI.ElementaryPositivity.QuantumTorus.intervalEventList_filter line 142
13. lemma OAI.ElementaryPositivity.QuantumTorus.event_not_retained line 148