Commit 2021-12-22 23:07 e15e015b

View on Github →

split(data/finset/sigma): Split off data.finset.basic (#10957) This moves finset.sigma to a new file data.finset.sigma. I'm crediting Mario for 16d40d7491d1fe8a733d21e90e516e0dd3f41c5b

Estimated changes

Modified src/data/finset/basic.lean

deleted theorem finset.mem_sigma

deleted theorem finset.sigma_eq_bUnion

deleted theorem finset.sigma_eq_empty

deleted theorem finset.sigma_mono

deleted theorem finset.sigma_nonempty

Modified src/data/finset/lattice.lean

deleted theorem finset.inf_sigma

deleted theorem finset.sup_sigma

Created src/data/finset/sigma.lean

added theorem finset.inf_sigma

added theorem finset.mem_sigma

added theorem finset.sigma_eq_bUnion

added theorem finset.sigma_eq_empty

added theorem finset.sigma_mono

added theorem finset.sigma_nonempty

added theorem finset.sup_sigma

Modified src/data/fintype/basic.lean