Commit 2024-12-05 01:28 639c1cb9

View on Github →

feat(Order/Bounds/Basic): Add basic order lemmas (#17595) This PR adds some simple lemmas about IsLeast/IsGreatest for images of sets along StrictMono/StrictAnti maps.

Estimated changes

Modified Mathlib/Order/Bounds/Image.lean

added theorem StrictAnti.map_isGreatest

added theorem StrictAnti.map_isLeast

added theorem StrictAnti.mem_lowerBounds_image

added theorem StrictAnti.mem_upperBounds_image

added theorem StrictMono.map_isGreatest

added theorem StrictMono.map_isLeast

added theorem StrictMono.mem_lowerBounds_image

added theorem StrictMono.mem_upperBounds_image