Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-27 07:49 eae3eadf

View on Github →

feat(topology/instances/ennreal): diameter of s : set real (#8433)

Estimated changes

Modified src/data/real/basic.lean

modified theorem real.Inf_empty

added theorem real.Inf_le_Sup

modified theorem real.Sup_empty

added theorem real.add_neg_lt_Sup

deleted theorem real.add_pos_lt_Sup

Modified src/topology/instances/ennreal.lean

added theorem metric.diam_closure

added theorem real.diam_eq

added theorem real.ediam_eq

Modified src/topology/instances/real.lean

added theorem real.subset_Icc_Inf_Sup_of_bounded

Modified src/topology/metric_space/basic.lean