Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded

Deprecated since 2026-01-08Use Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded instead.

∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  s.Nonempty → t.Nonempty → Bornology.IsBounded s → Bornology.IsBounded t → Metric.hausdorffEDist s t ≠ ⊤

Alias of Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded. If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance.

Defined in: Mathlib.Topology.MetricSpace.HausdorffDistance
Cited by: 0 results in Mathlib
Foundations: Depth 156 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.

Cites8

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

Setstatement · cited by 53,352
ENNRealstatement · cited by 9,879
Top.topstatement · cited by 9,680
Set.Nonemptystatement · cited by 2,627
PseudoMetricSpacestatement · cited by 1,550
Bornology.IsBoundedstatement · cited by 293
Metric.hausdorffEDiststatement · cited by 76
Metric.hausdorffEDist_ne_top_of_nonempty_of_boundedproof · cited by 4

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.