Commit 2024-02-20 17:52 bcc8209f

View on Github →

feat: iInter_sigma, biInter_sigma, biSup_sigma, biInf_sigma (#8964) similar to prod_sigma, prod_sigma', iInf_sigma, iInf_sigma', iSup_sigma, iSup_sigma' From PFR

Estimated changes

added theorem biInf_finsetSigma'
added theorem biInf_finsetSigma
added theorem biSup_finsetSigma'
added theorem biSup_finsetSigma
added theorem Set.iInter_sigma'
added theorem Set.iInter_sigma
added theorem Set.iUnion_sigma'
added theorem Set.iUnion_sigma
added theorem Set.biInter_sigma'
added theorem Set.biInter_sigma
added theorem Set.biUnion_sigma'
added theorem Set.biUnion_sigma
added theorem biInf_sigma'
added theorem biInf_sigma
added theorem biSup_sigma'
added theorem biSup_sigma