exists_edist_lt_of_hausdorffEdist_lt

English

If x ∈ s and the Hausdorff distance between s and t is less than r, then there exists y ∈ t with edist x y < r.

Русский

Если x ∈ s и расстояние Хаусдорфа между s и t меньше r, то существует y ∈ t такое, что edist x y < r.

LaTeX

$$$ (x \in s) \land (\operatorname{hausdorffEdist}(s,t) < r) \Rightarrow \exists y \in t, \operatorname{edist}(x,y) < r $$$

Lean4

/-- If the Hausdorff distance is `< r`, then any point in one of the sets has
a corresponding point at distance `< r` in the other set. -/
theorem exists_edist_lt_of_hausdorffEdist_lt {r : ℝ≥0∞} (h : x ∈ s) (H : hausdorffEdist s t < r) :
    ∃ y ∈ t, edist x y < r :=
  infEdist_lt_iff.mp <|
    calc
      infEdist x t ≤ hausdorffEdist s t := infEdist_le_hausdorffEdist_of_mem h
      _ < r := H

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