Commit 2022-12-16 03:51 91732b9d

View on Github →

feat port:Data.Set.Intervals.ProjIcc (#1051) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Intervals/ProjIcc.lean

added theorem Monotone.IccExtend

added def Set.IccExtend

added theorem Set.IccExtend_left

added theorem Set.IccExtend_of_le_left

added theorem Set.IccExtend_of_mem

added theorem Set.IccExtend_of_right_le

added theorem Set.IccExtend_range

added theorem Set.IccExtend_right

added theorem Set.Icc_extend_coe

added theorem Set.monotone_projIcc

added def Set.projIcc

added theorem Set.projIcc_eq_left

added theorem Set.projIcc_eq_right

added theorem Set.projIcc_left

added theorem Set.projIcc_of_le_left

added theorem Set.projIcc_of_mem

added theorem Set.projIcc_right

added theorem Set.projIcc_surjOn

added theorem Set.projIcc_surjective

added theorem Set.projIcc_val

added theorem Set.proj_Icc_of_right_le

added theorem Set.range_projIcc

added theorem Set.strictMonoOn_projIcc

added theorem StrictMono.strictMonoOn_IccExtend