Commit 2023-02-06 20:02 fac4de2e

View on Github →

feat: port Data.Sigma.Interval (#2114)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sigma/Interval.lean

added theorem Sigma.Icc_mk_mk

added theorem Sigma.Ico_mk_mk

added theorem Sigma.Ioc_mk_mk

added theorem Sigma.Ioo_mk_mk

added theorem Sigma.card_Icc

added theorem Sigma.card_Ico

added theorem Sigma.card_Ioc

added theorem Sigma.card_Ioo