OAI/Probability/FirstPassage/BKForcing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.ForcesBits line 9

   Also declared: OAI/Probability/GammaPassage/BKForcing.lean:10 (same declaration text).

2. lemma OAI.PlanarFPP.ForcesBits.positive_certificate line 12

   Also declared: OAI/Probability/GammaPassage/BKForcing.lean:13 (same declaration text).

3. theorem OAI.PlanarFPP.forcing_certificates_mem line 18

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

4. theorem OAI.PlanarFPP.finite_fair_BK_forcing line 33

   Also declared: OAI/Probability/GammaPassage/BKForcing.lean:34 (same declaration text).