Theorem Function.strictMono_of_rightInverse

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.strictMono_of_rightInverseView on Github →