Commit 2023-06-19 22:27 e266a22f

View on Github →

feat: More sup_indep lemmas (#5196) Match https://github.com/leanprover-community/mathlib/pull/11932

Estimated changes

modified theorem Set.pairwise_iUnion
added theorem Set.Disjoint.set_pi
added theorem Set.disjoint_pi
added theorem Set.pi_eq_empty_iff'
modified theorem Finset.SupIndep.attach
added theorem Finset.SupIndep.image
added theorem Finset.SupIndep.sigma
added theorem Finset.supIndep_attach
added theorem Finset.supIndep_map