OAI/Probability/StrongRayleigh/BinaryProjective.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem336AdditiveD139.binary_cylinder_isClosed line 14
2. theorem OAI.Problem336AdditiveD139.binary_cylinders_eventually_empty line 19
3. theorem OAI.Problem336AdditiveD139.binary_projective_exists line 32
4. theorem OAI.Problem336AdditiveD139.binary_projective_exists_unique line 71