Commit 2026-09-03 14:21 cd678173

View on Github →

chore(Order/Interval/Set/SuccPred): use to_dual (#43366) This PR uses to_dual in Mathlib.Order.Interval.Set.SuccPred. Some naming problems with Ico/Ioc were found and fixed.

Estimated changes

deleted theorem Set.Icc_pred_right_eq_Ico
deleted theorem Set.Iic_pred_eq_Iio
modified theorem Set.Iio_succ_eq_Iic
deleted theorem Set.Ioc_pred_left_eq_Icc
deleted theorem Set.Ioc_pred_pred_eq_Ico
deleted theorem Set.Ioc_pred_right_eq_Ioo
deleted theorem Set.Ioi_pred_eq_Ici
deleted theorem Set.Ioo_pred_left_eq_Ioc