Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 13:33 d742555c

View on Github →

feat(topology/instances/ennreal): diameter of intervals (#16556)

Estimated changes

added theorem real.diam_Icc
added theorem real.diam_Ico
added theorem real.diam_Ioc
added theorem real.diam_Ioo