OAI/Combinatorics/Chromatic/Walls/CompletedPathIndependence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ElementaryPositivity.RationalFiber.actualPathAction_independent line 20
2. def OAI.ElementaryPositivity.RationalFiber.completedTransport line 36
3. lemma OAI.ElementaryPositivity.RationalFiber.completedTransport_eq_path line 41
4. lemma OAI.ElementaryPositivity.RationalFiber.completedTransport_self line 50
5. lemma OAI.ElementaryPositivity.RationalFiber.completedTransport_trans line 57
6. def OAI.ElementaryPositivity.RationalFiber.comparisonWordHom line 79
7. lemma OAI.ElementaryPositivity.RationalFiber.comparisonWordHom_apply line 83
8. def OAI.ElementaryPositivity.RationalFiber.actualPathHom line 109
9. def OAI.ElementaryPositivity.RationalFiber.completedTransportEquiv line 172