Theorem Function.strictMonoOn_of_rightInvOn_of_mapsTo

Modification history

2026-08-31 16:15
Mathlib/Data/Set/Monotone.lean
feat(Data/Set): the right inverse of monotone is monotone (#41388) …
Added Function.strictMonoOn_of_rightInvOn_of_mapsToView on Github →