exists_dist_lt_of_hausdorffDist_lt'

English

Bounding Hausdorff distance by the diameter of the union: hausdorffDist(s, t) ≤ diam(s ∪ t) when s and t are nonempty and bounded.

Русский

Расстояние Хаусдорфа между непустыми ограниченными множествами не превосходит диаметр их объединения.

LaTeX

$$$\operatorname{hausdorffDist}(s,t) \le \operatorname{diam}(s\cup t) \quad (s,t\ \text{непустые, ограниченные}).$$$

Lean4

/-- If the Hausdorff distance is `< r`, any point in one of the sets is at distance
`< r` of a point in the other set. -/
theorem exists_dist_lt_of_hausdorffDist_lt' {r : ℝ} (h : y ∈ t) (H : hausdorffDist s t < r)
    (fin : hausdorffEdist s t ≠ ⊤) : ∃ x ∈ s, dist x y < r :=
  by
  rw [hausdorffDist_comm] at H
  rw [hausdorffEdist_comm] at fin
  simpa [dist_comm] using exists_dist_lt_of_hausdorffDist_lt h H fin

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