Commit 2024-11-23 06:30 1ef6e445

View on Github →

feat: image of any interval under affineHomeomorph (#19301)

Estimated changes

Modified Mathlib/Data/Set/Pointwise/Interval.lean

added theorem Set.image_affine_Ico

added theorem Set.image_affine_Ioc

added theorem Set.image_affine_Ioo

added theorem Set.image_mul_left_Ico

added theorem Set.image_mul_left_Ioc

added theorem Set.image_mul_right_Ico

added theorem Set.image_mul_right_Ioc

Modified Mathlib/Topology/Algebra/Field.lean

added theorem affineHomeomorph_image_Icc

added theorem affineHomeomorph_image_Ico

added theorem affineHomeomorph_image_Ioc

added theorem affineHomeomorph_image_Ioo