OAI/Combinatorics/Chromatic/Walls/MutatedHalfspaceTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.cutSide_affineSegment line 15
2. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.OnCutSide.trans line 32
3. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.OnCutSide.reindex line 40
4. lemma OAI.ElementaryPositivity.QuantumTorus.segmentBetween_onCutSide line 47
5. theorem OAI.ElementaryPositivity.QuantumTorus.generic_path_exists_onCutSide line 61
6. def OAI.ElementaryPositivity.QuantumTorus.endpointRatioPositive line 116
7. lemma OAI.ElementaryPositivity.QuantumTorus.endpointRatioPositive_nocut_cone line 127
8. theorem OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_rational_nocut line 154
9. theorem OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_nocut_loop line 171