hausdorffEdist_le_of_infEdist — Mathlib

English

If for all x in s we have infEdist x t ≤ r and for all x in t we have infEdist x s ≤ r, then hausdorffEdist s t ≤ r.

Русский

Если для всех x ∈ s выполняется infEdist x t ≤ r и для всех x ∈ t выполняется infEdist x s ≤ r, то hausdorffEdist s t ≤ r.

LaTeX

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

Lean4

/-- Bounding the Hausdorff edistance by bounding the edistance of any point
in each set to the other set -/
theorem hausdorffEdist_le_of_infEdist {r : ℝ≥0∞} (H1 : ∀ x ∈ s, infEdist x t ≤ r) (H2 : ∀ x ∈ t, infEdist x s ≤ r) :
    hausdorffEdist s t ≤ r := by
  simp only [hausdorffEdist_def, sup_le_iff, iSup_le_iff]
  exact ⟨H1, H2⟩

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