Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 09:57 626489ad

View on Github →

feat(topology/metric_space): diameter of a set in metric spaces (#651)

Estimated changes

Modified src/topology/metric_space/basic.lean

added theorem metric.bounded_iff_diam_ne_top

added def metric.diam

added theorem metric.diam_ball

added theorem metric.diam_closed_ball

added theorem metric.diam_empty

added theorem metric.diam_eq_zero_of_unbounded

added theorem metric.diam_le_of_forall_dist_le

added theorem metric.diam_mono

added theorem metric.diam_nonneg

added theorem metric.diam_singleton

added theorem metric.diam_union'

added theorem metric.diam_union

added theorem metric.dist_le_diam_of_mem

Modified src/topology/metric_space/emetric_space.lean

added def emetric.diam

added theorem emetric.diam_ball

added theorem emetric.diam_closed_ball

added theorem emetric.diam_empty

added theorem emetric.diam_le_of_forall_edist_le

added theorem emetric.diam_mono

added theorem emetric.diam_singleton

added theorem emetric.diam_union'

added theorem emetric.diam_union

added theorem emetric.edist_le_diam_of_mem