OAI/Combinatorics/Chromatic/Walls/MutatedPathIndependent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_independent line 24
2. def OAI.ElementaryPositivity.QuantumTorus.mutatedTransport line 41
3. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedTransport_eq_path line 48
4. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedTransport_self line 56
5. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedTransport_trans line 61
6. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedPathCompletion_pure line 92
7. lemma OAI.ElementaryPositivity.QuantumTorus.mutatedTransport_pure line 112
8. def OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.InRegion line 134
9. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.InRegion.trans line 140
10. lemma OAI.ElementaryPositivity.QuantumTorus.GenericLinePath.InRegion.castEnds line 148
11. lemma OAI.ElementaryPositivity.QuantumTorus.segmentBetween_inRegion line 154
12. lemma OAI.ElementaryPositivity.QuantumTorus.generic_region_path_via line 172