Theorem Function.monotoneOn_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) …
Modified Function.monotoneOn_of_rightInvOn_of_mapsToView on Github →
2024-10-04 14:05
Mathlib/Data/Set/Function.lean
chore(Data/Set): split Data/Set/Function (#17091) …
Modified Function.monotoneOn_of_rightInvOn_of_mapsToView on Github →
2024-01-06 09:51
Mathlib/Data/Set/Function.lean
chore(Set/Function): don't use `Sort _` (#9478) …
Modified Function.monotoneOn_of_rightInvOn_of_mapsToView on Github →
2022-12-26 11:29
Mathlib/Data/Set/Function.lean
feat: `Data.Set.Function` two lemmas about inverse of mono/antitone maps to sync with mathlib3#18001 (#1222) …
Added Function.monotoneOn_of_rightInvOn_of_mapsToView on Github →