Mathlib Map

Theorems · Definition · general topology

Metric.infEDist

{α : Type u} → [PseudoEMetricSpace α] → α → Set α → ENNReal

The minimal edistance of a point to a set

Defined in
Mathlib.Topology.MetricSpace.HausdorffDistance
Cited by
147 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.thickening · cited by 130Metric.thickeningMetric.cthickening · cited by 113Metric.cthickeningMetric.infDist · cited by 68Metric.infDistthickenedIndicatorAux · cited by 21thickenedIndicatorAuxMetric.hausdorffEDist_def · cited by 13Metric.hausdorffEDist_defMetric.infEDist_le_edist_of_mem · cited by 13Metric.infEDist_le_edist_…Metric.hausdorffEDist_comm · cited by 11Metric.hausdorffEDist_commMetric.infEDist_lt_iff · cited by 9Metric.infEDist_lt_iffMetric.continuous_infEDist · cited by 9Metric.continuous_infEDistMetric.infEDist_closure · cited by 8Metric.infEDist_closureMetric.infEDist_ne_top · cited by 8Metric.infEDist_ne_topMetric.infNndist · cited by 8Metric.infNndistMetric.cthickening_of_nonpos · cited by 8Metric.cthickening_of_non…Metric.infEDist_anti · cited by 7Metric.infEDist_antiMetric.infEDist_image · cited by 7Metric.infEDist_imageSet · cited by 53352SetENNReal · cited by 9879ENNRealiInf · cited by 1690iInfPseudoEMetricSpace · cited by 1536PseudoEMetricSpaceEDist.edist · cited by 735EDist.edistMetric.infEDistCITED BYCITES

Cites5

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

Cited by153

Results whose statement or proof uses this declaration.