mathlib

4e24c4bf - feat(data/set/intervals/proj_Icc): Extending from `Ici a` (#18795)

feat(data/set/intervals/proj_Icc): Extending from `Ici a` (#18795) Define the `Ici` and `Iic` versions of `set.proj_Icc`/`set.Icc_extend`. Slightly reorder the lemmas to allow better overall structure. This is useful for extending convex functions by a junk value.