OAI/Combinatorics/Chromatic/Walls/WallLineInitial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.finite_upper_bound line 16
2. lemma OAI.ElementaryPositivity.QuantumTorus.far_line_lex line 27
3. lemma OAI.ElementaryPositivity.QuantumTorus.offset_ray_generic line 50
4. theorem OAI.ElementaryPositivity.QuantumTorus.incoming_positive_at_far line 60
5. lemma OAI.ElementaryPositivity.FiniteEventTraversal.finite_gap line 96
6. lemma OAI.ElementaryPositivity.FiniteEventTraversal.near_not_mem line 114
7. theorem OAI.ElementaryPositivity.FiniteEventTraversal.descend line 127