Mathlib Map

Theorems · Definition · general topology

Metric.ediam

{X : Type u_2} → [PseudoEMetricSpace X] → Set X → ENNReal

The diameter of a set in a pseudoemetric space as an extended nonnegative real number.

Defined in
Mathlib.Topology.EMetricSpace.Diam
Cited by
159 results in Mathlib
Foundations
Depth 147 from the axioms, rests on 3,160 definitions · uses propext, Classical.choice, Quot.sound
Assumes
PseudoEMetricSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Metric.diam · cited by 74Metric.diamMetric.edist_le_ediam_of_mem · cited by 20Metric.edist_le_ediam_of_…MeasureTheory.OuterMeasure.mkMetric · cited by 15OuterMeasure.mkMetricMetric.ediam_mono · cited by 14Metric.ediam_monoMetric.ediam_le · cited by 13Metric.ediam_leIsometry.ediam_image · cited by 12Isometry.ediam_imageMetric.ediam_singleton · cited by 10Metric.ediam_singletonIsometry.diam_image · cited by 10Isometry.diam_imageMeasureTheory.OuterMeasure.mkMetric'.pre · cited by 9mkMetric'.preoscillationWithin · cited by 7oscillationWithinMetric.ediam_empty · cited by 7Metric.ediam_emptyMetric.ediam_subsingleton · cited by 6Metric.ediam_subsingletonMetric.isBounded_iff_ediam_ne_top · cited by 5Metric.isBounded_iff_edia…Bornology.IsBounded.ediam_ne_top · cited by 5IsBounded.ediam_ne_topMeasureTheory.Measure.hausdorffMeasure_zero_singleton · cited by 5Measure.hausdorffMeasure_…Set · cited by 53352SetENNReal · cited by 9879ENNRealiSup · cited by 2415iSupPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceEDist.edist · cited by 735EDist.edistMetric.ediamCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by166

Results whose statement or proof uses this declaration.