OAI/Probability/FirstPassage/BKFamilies.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.UpwardFamily line 11

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:11 (same declaration text).

2. def OAI.PlanarFPP.disjointOccurrenceFamily line 14

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

3. lemma OAI.PlanarFPP.mem_disjointOccurrenceFamily line 19

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:19 (same declaration text).

4. lemma OAI.PlanarFPP.disjointOccurrenceFamily_mono line 25

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:25 (same declaration text).

5. lemma OAI.PlanarFPP.UpwardFamily.nonMember line 32

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

6. lemma OAI.PlanarFPP.UpwardFamily.member line 44

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:44 (same declaration text).

7. lemma OAI.PlanarFPP.UpwardFamily.slice_subset line 56

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:56 (same declaration text).

8. lemma OAI.PlanarFPP.disjointOccurrence_nonMember line 63

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:63 (same declaration text).

9. lemma OAI.PlanarFPP.erase_subset_of_subset_insert line 76

   Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:76 (same declaration text).

10. lemma OAI.PlanarFPP.disjointOccurrence_member line 82

    Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:82 (same declaration text).

11. theorem OAI.PlanarFPP.finite_fair_BK line 119

    Also declared: OAI/Probability/GammaPassage/BKFamilies.lean:119 (same declaration text).