Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
set.nonempty_Icc_subtype
Modification history
2020-09-14 23:27
src/data/set/intervals/basic.lean
feat(topology/algebra/ordered): monotone continuous function is homeomorphism, relative version (#4043) …
Added
set.nonempty_Icc_subtype
View on Github →