Commit 2026-08-31 16:15 9a1d3bbd

View on Github →

feat(Data/Set): the right inverse of monotone is monotone (#41388) This PR adds some theorems about monotonicity of right inverse of some map. This is mainly for discoverability and includes a strict version of monotoneOn_of_rightInvOn_of_mapsTo i.e strictMonoOn_of_rightInvOn_of_mapsTo. Discussed here: Lemmas about StrictMono/Monotone maps with right inverse

Estimated changes

Modified Mathlib/Data/Set/Monotone.lean

added theorem Function.antitone_of_rightInverse

modified theorem Function.monotoneOn_of_rightInvOn_of_mapsTo

added theorem Function.monotone_of_rightInverse

added theorem Function.strictAntiOn_of_rightInvOn_of_mapsTo

added theorem Function.strictAnti_of_rightInverse

added theorem Function.strictMonoOn_of_rightInvOn_of_mapsTo

added theorem Function.strictMono_of_rightInverse