Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.nonempty_Ico_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_Ico_subtypeView on Github →