Commit 2023-09-28 12:57 dae39b2a

View on Github →

feat(Data/Set/Intervals/Image): Complete API (#7146) Dualise all existing lemmas and prove their strictly monotone versions. The lemmas are grouped as

  • mapsTo, image_subset
    • On, not On
      • Monotone, Antitone, StrictMono, StrictAnti
        • Ixi, Iix, Ixx

Estimated changes

added theorem Antitone.mapsTo_Icc
added theorem Antitone.mapsTo_Ici
added theorem Antitone.mapsTo_Iic
added theorem AntitoneOn.mapsTo_Icc
added theorem AntitoneOn.mapsTo_Ici
added theorem AntitoneOn.mapsTo_Iic
modified theorem Monotone.image_Icc_subset
modified theorem Monotone.image_Ici_subset
modified theorem Monotone.image_Iic_subset
modified theorem Monotone.mapsTo_Icc
modified theorem Monotone.mapsTo_Ici
modified theorem Monotone.mapsTo_Iic
added theorem MonotoneOn.mapsTo_Icc
added theorem MonotoneOn.mapsTo_Ici
added theorem MonotoneOn.mapsTo_Iic
added theorem StrictAnti.mapsTo_Ico
added theorem StrictAnti.mapsTo_Iio
added theorem StrictAnti.mapsTo_Ioc
added theorem StrictAnti.mapsTo_Ioi
added theorem StrictAnti.mapsTo_Ioo
modified theorem StrictMono.image_Iio_subset
modified theorem StrictMono.image_Ioi_subset
modified theorem StrictMono.image_Ioo_subset
modified theorem StrictMono.mapsTo_Ico
modified theorem StrictMono.mapsTo_Iio
modified theorem StrictMono.mapsTo_Ioc
modified theorem StrictMono.mapsTo_Ioi
modified theorem StrictMono.mapsTo_Ioo
added theorem Antitone.mapsTo_uIcc
added theorem AntitoneOn.mapsTo_uIcc
added theorem Monotone.mapsTo_uIcc
added theorem MonotoneOn.mapsTo_uIcc
added theorem AntitoneOn.map_inf
added theorem AntitoneOn.map_sup
added theorem MonotoneOn.map_inf
added theorem MonotoneOn.map_sup