infEdist_le_hausdorffEdist_of_mem

English

If x ∈ s, then the distance from x to t is bounded above by the Hausdorff distance between s and t.

Русский

Если x ∈ s, то расстояние от x до t не превышает расстояния Хаусдорфа между s и t.

LaTeX

$$$ (x \in s) \Rightarrow \operatorname{infEdist}(x,t) \le \operatorname{hausdorffEdist}(s,t) $$$

Lean4

/-- The distance to a set is controlled by the Hausdorff distance. -/
theorem infEdist_le_hausdorffEdist_of_mem (h : x ∈ s) : infEdist x t ≤ hausdorffEdist s t :=
  by
  rw [hausdorffEdist_def]
  refine le_trans ?_ le_sup_left
  exact le_iSup₂ (α := ℝ≥0∞) x h

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