OAI/Probability/FirstPassage/OrientedCompactness.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.orientedSurvival line 9

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:14 (same declaration text).

2. def OAI.PlanarFPP.infiniteOrientedPath line 13

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:18 (same declaration text).

3. theorem OAI.PlanarFPP.orientedSurvival_pred line 17

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:22 (same declaration text).

4. theorem OAI.PlanarFPP.orientedSurvival_mono line 27

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:32 (same declaration text).

5. theorem OAI.PlanarFPP.oriented_surviving_successor line 33

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:38 (same declaration text).

6. theorem OAI.PlanarFPP.infiniteOrientedPath_iff line 44

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:49 (same declaration text).

7. def OAI.PlanarFPP.orientedEndpoints line 74

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:79 (same declaration text).

8. theorem OAI.PlanarFPP.orientedEndpoints_nonempty_iff line 80

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:85 (same declaration text).

9. def OAI.PlanarFPP.orientedReachable line 88

   Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:95 (same declaration text).

10. theorem OAI.PlanarFPP.orientedReachable_finite_of_no_infinite_path line 91

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:98 (same declaration text).

11. theorem OAI.PlanarFPP.orientedReachable_origin line 107

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:114 (same declaration text).

12. theorem OAI.PlanarFPP.orientedEndpoints_extend line 110

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:118 (same declaration text).

13. theorem OAI.PlanarFPP.orientedReachable_forward line 129

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:138 (same declaration text).

14. theorem OAI.PlanarFPP.orientedReachable_boundary_bad line 136

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:146 (same declaration text).

15. theorem OAI.PlanarFPP.measurableSet_orientedSurvival line 145

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:155 (same declaration text).

16. theorem OAI.PlanarFPP.measurableSet_infiniteOrientedPath line 152

    Also declared: OAI/Probability/GammaPassage/OrientedCompactness.lean:162 (same declaration text).