Mathlib v3 is deprecated. Go to Mathlib v4

Theorem surj_on_Icc_of_monotone_surjective

Modification history

2020-08-26 16:20

src/data/set/intervals/surj_on.lean

feat(topology/algebra/ordered): conditions for a strictly monotone function to be a homeomorphism (#3843) …

Added surj_on_Icc_of_monotone_surjective View on Github →