Commit 2023-06-02 19:15 c9c1578f

View on Github →

feat: port Probability.Independence.ZeroOne (#4606)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Probability/Independence/Basic.lean

Created Mathlib/Probability/Independence/ZeroOne.lean

added theorem ProbabilityTheory.indep_biSup_compl

added theorem ProbabilityTheory.indep_biSup_limsup

added theorem ProbabilityTheory.indep_iSup_directed_limsup

added theorem ProbabilityTheory.indep_iSup_limsup

added theorem ProbabilityTheory.indep_limsup_atBot_self

added theorem ProbabilityTheory.indep_limsup_atTop_self

added theorem ProbabilityTheory.indep_limsup_self

added theorem ProbabilityTheory.measure_eq_zero_or_one_of_indepSetCat_self

added theorem ProbabilityTheory.measure_eq_zero_or_one_or_top_of_indepSet_self

added theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup

added theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atBot

added theorem ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop