Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 21:33 aafc4861

View on Github →

feat(topology/ordered): intervals frontiers (#3617) from the sphere eversion project

Estimated changes

added theorem closure_Icc
added theorem closure_Ici
modified theorem closure_Ico
added theorem closure_Iic
modified theorem closure_Iio
modified theorem closure_Ioc
modified theorem closure_Ioi
modified theorem closure_Ioo
added theorem frontier_Icc
added theorem frontier_Ici
added theorem frontier_Ico
added theorem frontier_Iic
added theorem frontier_Iio
added theorem frontier_Ioc
added theorem frontier_Ioi
added theorem frontier_Ioo