Commit 2023-01-17 12:10 5b2314fa

View on Github →

feat: port Data.Finset.Sigma (#1620)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Sigma.lean

added theorem Finset.card_sigmaLift

added theorem Finset.coe_sigma

added theorem Finset.disjUnionᵢ_map_sigma_mk

added theorem Finset.inf_sigma

added theorem Finset.mem_sigma

added theorem Finset.mem_sigmaLift

added theorem Finset.mk_mem_sigmaLift

added theorem Finset.not_mem_sigmaLift_of_ne_left

added theorem Finset.not_mem_sigmaLift_of_ne_right

added theorem Finset.pairwiseDisjoint_map_sigmaMk

added def Finset.sigmaLift

added theorem Finset.sigmaLift_eq_empty

added theorem Finset.sigmaLift_mono

added theorem Finset.sigmaLift_nonempty

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 Mathlib/Logic/Embedding/Basic.lean