Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-11 15:46 4e24c4bf

View on Github →

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.

Estimated changes

deleted theorem monotone.Icc_extend
added theorem set.Icc_extend_apply
added def set.Ici_extend
added theorem set.Ici_extend_apply
added theorem set.Ici_extend_coe
added theorem set.Ici_extend_of_le
added theorem set.Ici_extend_of_mem
added theorem set.Ici_extend_self
added def set.Iic_extend
added theorem set.Iic_extend_apply
added theorem set.Iic_extend_coe
added theorem set.Iic_extend_of_le
added theorem set.Iic_extend_of_mem
added theorem set.Iic_extend_self
added theorem set.coe_proj_Icc
added theorem set.coe_proj_Ici
added theorem set.coe_proj_Iic
added theorem set.monotone_proj_Ici
added theorem set.monotone_proj_Iic
modified theorem set.proj_Icc_surjective
added def set.proj_Ici
added theorem set.proj_Ici_coe
added theorem set.proj_Ici_eq_self
added theorem set.proj_Ici_of_le
added theorem set.proj_Ici_of_mem
added theorem set.proj_Ici_self
added theorem set.proj_Ici_surj_on
added def set.proj_Iic
added theorem set.proj_Iic_coe
added theorem set.proj_Iic_eq_self
added theorem set.proj_Iic_of_le
added theorem set.proj_Iic_of_mem
added theorem set.proj_Iic_self
added theorem set.proj_Iic_surj_on
added theorem set.range_Ici_extend
added theorem set.range_Iic_extend
modified theorem set.range_proj_Icc
added theorem set.range_proj_Ici
added theorem set.range_proj_Iic