Commit 2023-05-01 15:10 4476679b

View on Github →

feat: f.update i '' Icc a b = Icc (f.update i a) (f.update i b) (#3747) Match https://github.com/leanprover-community/mathlib/pull/18892

Estimated changes

Modified Mathlib/Algebra/Group/Pi.lean

added theorem Pi.mulSingle_inf

added theorem Pi.mulSingle_sup

Modified Mathlib/Data/Set/Intervals/Pi.lean

added theorem Set.image_mulSingle_Icc

added theorem Set.image_mulSingle_Icc_left

added theorem Set.image_mulSingle_Icc_right

added theorem Set.image_mulSingle_Ico

added theorem Set.image_mulSingle_Ico_left

added theorem Set.image_mulSingle_Ico_right

added theorem Set.image_mulSingle_Ioc

added theorem Set.image_mulSingle_Ioc_left

added theorem Set.image_mulSingle_Ioc_right

added theorem Set.image_mulSingle_Ioo

added theorem Set.image_mulSingle_Ioo_left

added theorem Set.image_mulSingle_Ioo_right

added theorem Set.image_mulSingle_uIcc

added theorem Set.image_mulSingle_uIcc_left

added theorem Set.image_mulSingle_uIcc_right

added theorem Set.image_update_Icc

added theorem Set.image_update_Icc_left

added theorem Set.image_update_Icc_right

added theorem Set.image_update_Ico

added theorem Set.image_update_Ico_left

added theorem Set.image_update_Ico_right

added theorem Set.image_update_Ioc

added theorem Set.image_update_Ioc_left

added theorem Set.image_update_Ioc_right

added theorem Set.image_update_Ioo

added theorem Set.image_update_Ioo_left

added theorem Set.image_update_Ioo_right

added theorem Set.image_update_uIcc

added theorem Set.image_update_uIcc_left

added theorem Set.image_update_uIcc_right

Modified Mathlib/Order/Lattice.lean

added theorem Function.update_inf

added theorem Function.update_sup