Theorems · Theorem · general topology

Metric.hausdorffDist_le_diam

∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  s.Nonempty →
    Bornology.IsBounded s → t.Nonempty → Bornology.IsBounded t → Metric.hausdorffDist s t ≤ Metric.diam (s ∪ t)

The Hausdorff distance is controlled by the diameter of the union.

Defined in: Mathlib.Topology.MetricSpace.HausdorffDistance
Cited by: 0 results in Mathlib
Foundations: Depth 159 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites13

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

Setstatement and proof · cited by 53,352
Realstatement · cited by 25,697
Set.Nonemptystatement and proof · cited by 2,627
PseudoMetricSpacestatement and proof · cited by 1,550
Bornology.IsBoundedstatement and proof · cited by 293
Set.subset_union_leftproof · cited by 142
Set.subset_union_rightproof · cited by 123
Metric.diamstatement · cited by 74
Metric.hausdorffDiststatement · cited by 30
Metric.dist_le_diam_of_memproof · cited by 14
Bornology.IsBounded.unionproof · cited by 8
Metric.diam_nonnegproof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.