infDist_le_hausdorffDist_of_mem — Mathlib

English

The distance from a point to a set is controlled by the Hausdorff distance between the two sets.

Русский

Расстояние от точки до множества контролируется расстоянием Хаусдорфа между двумя множестами.

LaTeX

$$$\operatorname{infDist}(x,t) \le \operatorname{hausdorffDist}(s,t) \quad \text{whenever } x\in s.$$$

Lean4

/-- The distance to a set is controlled by the Hausdorff distance. -/
theorem infDist_le_hausdorffDist_of_mem (hx : x ∈ s) (fin : hausdorffEdist s t ≠ ⊤) : infDist x t ≤ hausdorffDist s t :=
  toReal_mono fin (infEdist_le_hausdorffEdist_of_mem hx)

Похожие утверждения