Theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop

Modification history

2024-09-03 08:22
Mathlib/Probability/Independence/ZeroOne.lean
feat: remove many `IsMarkovKernel` and `IsProbabilityMeasure` assumptions (#16399) …
Modified ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTopView on Github →
2024-08-09 00:58
Mathlib/Probability/Independence/ZeroOne.lean
chore: backports for leanprover/lean4#4814 (part 34) (#15607)
Modified ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTopView on Github →
2023-06-02 19:15
Mathlib/Probability/Independence/ZeroOne.lean
feat: port Probability.Independence.ZeroOne (#4606)
Added ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTopView on Github →