Commit 2023-10-30 08:37 0b6d797c

View on Github →

feat(Data/Set): images of intervals under Subtype.val (#7653) Add simp lemmas for images of intervals in other intervals under Subtype.val.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean

Modified Mathlib/Data/Set/Intervals/Image.lean

added theorem Set.image_subtype_val_Icc_Ici

added theorem Set.image_subtype_val_Icc_Iic

added theorem Set.image_subtype_val_Icc_Iio

added theorem Set.image_subtype_val_Icc_Ioi

added theorem Set.image_subtype_val_Ici_Ici

added theorem Set.image_subtype_val_Ici_Iic

added theorem Set.image_subtype_val_Ici_Iio

added theorem Set.image_subtype_val_Ici_Ioi

added theorem Set.image_subtype_val_Ico_Ici

added theorem Set.image_subtype_val_Ico_Iic

added theorem Set.image_subtype_val_Ico_Iio

added theorem Set.image_subtype_val_Ico_Ioi

added theorem Set.image_subtype_val_Iic_Ici

added theorem Set.image_subtype_val_Iic_Iic

added theorem Set.image_subtype_val_Iic_Iio

added theorem Set.image_subtype_val_Iic_Ioi

added theorem Set.image_subtype_val_Iio_Ici

added theorem Set.image_subtype_val_Iio_Iic

added theorem Set.image_subtype_val_Iio_Iio

added theorem Set.image_subtype_val_Iio_Ioi

added theorem Set.image_subtype_val_Ioc_Ici

added theorem Set.image_subtype_val_Ioc_Iic

added theorem Set.image_subtype_val_Ioc_Iio

added theorem Set.image_subtype_val_Ioc_Ioi

added theorem Set.image_subtype_val_Ioi_Ici

added theorem Set.image_subtype_val_Ioi_Iic

added theorem Set.image_subtype_val_Ioi_Iio

added theorem Set.image_subtype_val_Ioi_Ioi

added theorem Set.image_subtype_val_Ioo_Ici

added theorem Set.image_subtype_val_Ioo_Iic

added theorem Set.image_subtype_val_Ioo_Iio

added theorem Set.image_subtype_val_Ioo_Ioi

added theorem Set.preimage_subtype_val_Icc

added theorem Set.preimage_subtype_val_Ici

added theorem Set.preimage_subtype_val_Ico

added theorem Set.preimage_subtype_val_Iic

added theorem Set.preimage_subtype_val_Iio

added theorem Set.preimage_subtype_val_Ioc

added theorem Set.preimage_subtype_val_Ioi

added theorem Set.preimage_subtype_val_Ioo

Modified Mathlib/Data/Set/Intervals/OrdConnected.lean

added theorem Set.image_subtype_val_Icc

added theorem Set.image_subtype_val_Ico

added theorem Set.image_subtype_val_Ioc

added theorem Set.image_subtype_val_Ioo