Commit 2023-01-03 02:50 95c8c7e5

View on Github →

feat: port Data.Set.Intervals.Monotone (#1294) Surprising tricky for a beginner O_O -- had to figure out that rename_i was a thing.

Estimated changes

Modified Mathlib.lean

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

added theorem StrictMonoOn.Iic_id_le

added theorem StrictMonoOn.Iic_le_id

added theorem antitone_Ici

added theorem antitone_Ioi

added theorem monotone_Iic

added theorem monotone_Iio

added theorem strictAntiOn_Iic_of_lt_pred

added theorem strictAntiOn_Iic_of_succ_lt

added theorem strictMonoOn_Iic_of_lt_succ

added theorem strictMonoOn_Iic_of_pred_lt

added theorem unionᵢ_Ioo_of_mono_of_isGLB_of_isLUB