mathlib3
0b045c73 - chore(probability/independence): simplify the definition of pi_Union_Inter (#17043)

Commit
3 years ago
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.
Author
Parents
Loading