Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-16 08:34 c4c2ed62

View on Github →

feat(order/sup_indep): More lemmas (#11932) A few more lemmas about finset.sup_indep and set.pairwise_disjoint.

Estimated changes

modified theorem set.pairwise_Union
added theorem disjoint.set_pi
added theorem disjoint.set_prod_left
added theorem set.disjoint_pi
modified theorem set.disjoint_prod
added theorem set.pi_eq_empty_iff'
modified theorem finset.sup_indep.attach
added theorem finset.sup_indep.image
added theorem finset.sup_indep.sigma
added theorem finset.sup_indep_map