Commit 2023-01-31 19:04 29ffa06c

View on Github →

feat: port Data.Sum.Interval (#1962)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Sum/Interval.lean

added theorem Finset.inl_mem_sumLift₂

added theorem Finset.inr_mem_sumLift₂

added theorem Finset.mem_sumLift₂

added def Finset.sumLift₂

added theorem Finset.sumLift₂_eq_empty

added theorem Finset.sumLift₂_mono

added theorem Finset.sumLift₂_nonempty

added theorem Sum.Icc_inl_inl

added theorem Sum.Icc_inl_inr

added theorem Sum.Icc_inr_inl

added theorem Sum.Icc_inr_inr

added theorem Sum.Ico_inl_inl

added theorem Sum.Ico_inl_inr

added theorem Sum.Ico_inr_inl

added theorem Sum.Ico_inr_inr

added theorem Sum.Ioc_inl_inl

added theorem Sum.Ioc_inl_inr

added theorem Sum.Ioc_inr_inl

added theorem Sum.Ioc_inr_inr

added theorem Sum.Ioo_inl_inl

added theorem Sum.Ioo_inl_inr

added theorem Sum.Ioo_inr_inl

added theorem Sum.Ioo_inr_inr