Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-06 10:42 a23c47ca

View on Github →

feat(topology/instances/ennreal): ediam of intervals (#8546)

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.zero_eq_of_real

Modified src/topology/instances/ennreal.lean

added theorem ennreal.tendsto_finset_prod_of_ne_top

modified theorem real.diam_eq

added theorem real.ediam_Icc

added theorem real.ediam_Ico

added theorem real.ediam_Ioc

added theorem real.ediam_Ioo

modified theorem real.ediam_eq

Modified src/topology/metric_space/emetric_space.lean

added theorem edist_pi_le_iff

added theorem emetric.diam_pi_le_of_le

Modified src/topology/metric_space/holder.lean