Commit 2026-09-08 16:08 581efaab

View on Github →

chore(Order/Interval/Set/Image): use to_dual (#43584)

Estimated changes

Modified Mathlib/Order/Interval/Set/Image.lean

deleted theorem Antitone.image_Iic_subset

deleted theorem Antitone.mapsTo_Iic

deleted theorem AntitoneOn.image_Iic_subset

deleted theorem AntitoneOn.mapsTo_Iic

deleted theorem Monotone.image_Iic_subset

deleted theorem Monotone.mapsTo_Iic

deleted theorem MonotoneOn.image_Iic_subset

deleted theorem MonotoneOn.mapsTo_Iic

deleted theorem Set.image_subtype_val_Ici_subset

deleted theorem Set.image_subtype_val_Iic_Ici

deleted theorem Set.image_subtype_val_Iic_Iic

deleted theorem Set.image_subtype_val_Iic_Iio

deleted theorem Set.image_subtype_val_Iic_Ioi

modified theorem Set.image_subtype_val_Iic_subset

deleted theorem Set.image_subtype_val_Iio_Ici

deleted theorem Set.image_subtype_val_Iio_Iic

deleted theorem Set.image_subtype_val_Iio_Iio

deleted theorem Set.image_subtype_val_Iio_Ioi

modified theorem Set.image_subtype_val_Iio_subset

deleted theorem Set.image_subtype_val_Ioc_subset

deleted theorem Set.image_subtype_val_Ioi_subset

modified theorem Set.preimage_subtype_val_Icc

modified theorem Set.preimage_subtype_val_Ici

modified theorem Set.preimage_subtype_val_Ico

deleted theorem Set.preimage_subtype_val_Iic

deleted theorem Set.preimage_subtype_val_Iio

deleted theorem Set.preimage_subtype_val_Ioc

modified theorem Set.preimage_subtype_val_Ioi

modified theorem Set.preimage_subtype_val_Ioo

deleted theorem StrictAnti.image_Iio_subset

deleted theorem StrictAnti.image_Ioc_subset

deleted theorem StrictAnti.mapsTo_Iio

deleted theorem StrictAnti.mapsTo_Ioc

deleted theorem StrictAntiOn.image_Iio_subset

deleted theorem StrictAntiOn.image_Ioc_subset

deleted theorem StrictAntiOn.mapsTo_Iio

deleted theorem StrictAntiOn.mapsTo_Ioc

deleted theorem StrictMono.image_Iio_subset

deleted theorem StrictMono.image_Ioc_subset

deleted theorem StrictMono.mapsTo_Iio

deleted theorem StrictMono.mapsTo_Ioc

deleted theorem StrictMonoOn.image_Iio_subset

deleted theorem StrictMonoOn.image_Ioc_subset

deleted theorem StrictMonoOn.mapsTo_Iio

deleted theorem StrictMonoOn.mapsTo_Ioc

deleted theorem directedOn_ge_Icc

deleted theorem directedOn_ge_Ici

deleted theorem directedOn_ge_Ico

modified theorem directedOn_le_Iic