Commit 2022-10-19 04:48 0b045c73

View on Github →

chore(probability/independence): simplify the definition of pi_Union_Inter (#17043) Due to the simplification, sup_closed is no longer useful. Since it was introduced for this application and is not used anywhere else, I removed it.

Estimated changes

Modified src/data/set/lattice.lean

deleted theorem sup_closed.inter

deleted def sup_closed

deleted theorem sup_closed_of_linear_order

deleted theorem sup_closed_of_totally_ordered

deleted theorem sup_closed_singleton

Modified src/measure_theory/pi_system.lean

added theorem generate_from_pi_Union_Inter_measurable_set

deleted theorem generate_from_pi_Union_Inter_measurable_space

deleted theorem generate_from_pi_Union_Inter_subsets

modified def pi_Union_Inter

modified theorem subset_pi_Union_Inter

Modified src/probability/independence.lean

deleted theorem probability_theory.Indep_sets.Indep_aux

modified theorem probability_theory.indep_sets_pi_Union_Inter_of_disjoint