OAI/Probability/FirstPassage/PathSubpaths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarFPP.pathIn_append_left line 10
2. lemma OAI.PlanarFPP.pathIn_append_right line 16
3. lemma OAI.PlanarFPP.reverseSteps_append line 23
4. lemma OAI.PlanarFPP.reverseSteps_reverse line 26
5. lemma OAI.PlanarFPP.pathIn_reverseSteps line 30
6. lemma OAI.PlanarFPP.path_first_column_up line 51
7. lemma OAI.PlanarFPP.path_first_column_down line 73