Mathlib.Topology.MetricSpace.HausdorffDistance

EMetric.infEdist definition

(x : α) (s : Set α) : ℝ≥0∞

Full source

/-- The minimal edistance of a point to a set -/
def infEdist (x : α) (s : Set α) : ℝ≥0∞ :=
  ⨅ y ∈ s, edist x y

Minimal extended distance from a point to a set

Informal description

Given a point $x$ in an extended metric space and a subset $s$ of the space, the minimal extended distance from $x$ to $s$ is defined as the infimum of the extended distances from $x$ to all points $y$ in $s$, denoted by $\inf_{y \in s} d(x, y)$. This value is an element of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EMetric.infEdist_empty theorem

: infEdist x ∅ = ∞

Full source

@[simp]
theorem infEdist_empty : infEdist x ∅ = ∞ :=
  iInf_emptyset

Minimal Extended Distance to Empty Set is Infinity

Informal description

For any point $x$ in an extended metric space, the minimal extended distance from $x$ to the empty set is $\infty$, i.e., $\inf_{y \in \emptyset} d(x, y) = \infty$.

EMetric.le_infEdist theorem

{d} : d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y

Full source

theorem le_infEdist {d} : d ≤ infEdist x s ↔ ∀ y ∈ s, d ≤ edist x y := by
  simp only [infEdist, le_iInf_iff]

Characterization of Minimal Extended Distance via Pointwise Inequality

Informal description

For any extended nonnegative real number $d$, the inequality $d \leq \inf_{y \in s} d(x, y)$ holds if and only if for every point $y$ in the set $s$, the extended distance $d(x, y)$ is at least $d$.

EMetric.infEdist_union theorem

: infEdist x (s ∪ t) = infEdist x s ⊓ infEdist x t

Full source

/-- The edist to a union is the minimum of the edists -/
@[simp]
theorem infEdist_union : infEdist x (s ∪ t) = infEdistinfEdist x s ⊓ infEdist x t :=
  iInf_union

Minimal Distance to Union is Minimum of Minimal Distances

Informal description

For any point $x$ in an extended metric space and any two subsets $s$ and $t$ of the space, the minimal extended distance from $x$ to the union $s \cup t$ is equal to the minimum of the minimal extended distances from $x$ to $s$ and from $x$ to $t$. In symbols: \[ \inf_{y \in s \cup t} d(x, y) = \min\left(\inf_{y \in s} d(x, y), \inf_{y \in t} d(x, y)\right). \]

EMetric.infEdist_iUnion theorem

(f : ι → Set α) (x : α) : infEdist x (⋃ i, f i) = ⨅ i, infEdist x (f i)

Full source

@[simp]
theorem infEdist_iUnion (f : ι → Set α) (x : α) : infEdist x (⋃ i, f i) = ⨅ i, infEdist x (f i) :=
  iInf_iUnion f _

Minimal Distance to Union Equals Infimum of Minimal Distances

Informal description

For any indexed family of sets $(f_i)_{i \in \iota}$ in an extended metric space and any point $x$ in the space, the minimal extended distance from $x$ to the union $\bigcup_i f_i$ is equal to the infimum of the minimal extended distances from $x$ to each individual set $f_i$. In symbols: \[ \inf_{y \in \bigcup_i f_i} d(x, y) = \inf_i \inf_{y \in f_i} d(x, y) \]

EMetric.infEdist_biUnion theorem

{ι : Type*} (f : ι → Set α) (I : Set ι) (x : α) : infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i)

Full source

lemma infEdist_biUnion {ι : Type*} (f : ι → Set α) (I : Set ι) (x : α) :
    infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i) := by simp only [infEdist_iUnion]

Minimal Distance to Bounded Union Equals Infimum of Minimal Distances

Informal description

For any indexed family of sets $(f_i)_{i \in \iota}$ in an extended metric space, any subset $I \subseteq \iota$, and any point $x$ in the space, the minimal extended distance from $x$ to the union $\bigcup_{i \in I} f_i$ is equal to the infimum of the minimal extended distances from $x$ to each individual set $f_i$ for $i \in I$. In symbols: \[ \inf_{y \in \bigcup_{i \in I} f_i} d(x, y) = \inf_{i \in I} \inf_{y \in f_i} d(x, y). \]

EMetric.infEdist_singleton theorem

: infEdist x { y } = edist x y

Full source

/-- The edist to a singleton is the edistance to the single point of this singleton -/
@[simp]
theorem infEdist_singleton : infEdist x {y} = edist x y :=
  iInf_singleton

Minimal Extended Distance to Singleton Equals Point Distance

Informal description

For any point $x$ in an extended metric space and a singleton set $\{y\}$, the minimal extended distance from $x$ to $\{y\}$ is equal to the extended distance between $x$ and $y$, i.e., \[ \inf_{z \in \{y\}} d(x, z) = d(x, y). \]

EMetric.infEdist_le_edist_of_mem theorem

(h : y ∈ s) : infEdist x s ≤ edist x y

Full source

/-- The edist to a set is bounded above by the edist to any of its points -/
theorem infEdist_le_edist_of_mem (h : y ∈ s) : infEdist x s ≤ edist x y :=
  iInf₂_le y h

Minimal Extended Distance to Set is Bounded by Distance to Any Point in the Set

Informal description

For any point $x$ in an extended metric space and any subset $s$ of the space, if $y$ is a point in $s$, then the minimal extended distance from $x$ to $s$ is less than or equal to the extended distance from $x$ to $y$, i.e., \[ \inf_{z \in s} d(x, z) \leq d(x, y). \]

EMetric.infEdist_zero_of_mem theorem

(h : x ∈ s) : infEdist x s = 0

Full source

/-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
theorem infEdist_zero_of_mem (h : x ∈ s) : infEdist x s = 0 :=
  nonpos_iff_eq_zero.1 <| @edist_self _ _ x ▸ infEdist_le_edist_of_mem h

Minimal Extended Distance to Set is Zero for Points in the Set

Informal description

For any point $x$ in an extended metric space and any subset $s$ of the space, if $x$ belongs to $s$, then the minimal extended distance from $x$ to $s$ is zero, i.e., \[ \inf_{y \in s} d(x, y) = 0. \]

EMetric.infEdist_anti theorem

(h : s ⊆ t) : infEdist x t ≤ infEdist x s

Full source

/-- The edist is antitone with respect to inclusion. -/
theorem infEdist_anti (h : s ⊆ t) : infEdist x t ≤ infEdist x s :=
  iInf_le_iInf_of_subset h

Monotonicity of Minimal Extended Distance with Respect to Set Inclusion

Informal description

For any point $x$ in an extended metric space and subsets $s$ and $t$ of the space such that $s \subseteq t$, the minimal extended distance from $x$ to $t$ is less than or equal to the minimal extended distance from $x$ to $s$, i.e., \[ \inf_{y \in t} d(x, y) \leq \inf_{y \in s} d(x, y). \]

EMetric.infEdist_lt_iff theorem

{r : ℝ≥0∞} : infEdist x s < r ↔ ∃ y ∈ s, edist x y < r

Full source

/-- The edist to a set is `< r` iff there exists a point in the set at edistance `< r` -/
theorem infEdist_lt_iff {r : ℝ≥0∞} : infEdistinfEdist x s < r ↔ ∃ y ∈ s, edist x y < r := by
  simp_rw [infEdist, iInf_lt_iff, exists_prop]

Characterization of Minimal Extended Distance via Point in Set: $\inf_{y \in s} d(x, y) < r \leftrightarrow \exists y \in s, d(x, y) < r$

Informal description

For any extended nonnegative real number $r$, the minimal extended distance $\inf_{y \in s} d(x, y)$ from a point $x$ to a set $s$ is less than $r$ if and only if there exists a point $y \in s$ such that the extended distance $d(x, y) < r$.

EMetric.infEdist_le_infEdist_add_edist theorem

: infEdist x s ≤ infEdist y s + edist x y

Full source

/-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
the edist from `x` to `y` -/
theorem infEdist_le_infEdist_add_edist : infEdist x s ≤ infEdist y s + edist x y :=
  calc
    ⨅ z ∈ s, edist x z ≤ ⨅ z ∈ s, edist y z + edist x y :=
      iInf₂_mono fun _ _ => (edist_triangle _ _ _).trans_eq (add_comm _ _)
    _ = (⨅ z ∈ s, edist y z) + edist x y := by simp only [ENNReal.iInf_add]

Triangle Inequality for Minimal Extended Distance: $\inf_{z \in s} d(x, z) \leq \inf_{z \in s} d(y, z) + d(x, y)$

Informal description

For any points $x$ and $y$ in an extended metric space and any subset $s$ of the space, the minimal extended distance from $x$ to $s$ is bounded above by the sum of the minimal extended distance from $y$ to $s$ and the extended distance between $x$ and $y$, i.e., \[ \inf_{z \in s} d(x, z) \leq \inf_{z \in s} d(y, z) + d(x, y). \]

EMetric.infEdist_le_edist_add_infEdist theorem

: infEdist x s ≤ edist x y + infEdist y s

Full source

theorem infEdist_le_edist_add_infEdist : infEdist x s ≤ edist x y + infEdist y s := by
  rw [add_comm]
  exact infEdist_le_infEdist_add_edist

Triangle Inequality for Minimal Extended Distance (Symmetric Form)

Informal description

For any points $x$ and $y$ in an extended metric space and any subset $s$ of the space, the minimal extended distance from $x$ to $s$ is bounded above by the sum of the extended distance between $x$ and $y$ and the minimal extended distance from $y$ to $s$, i.e., \[ \inf_{z \in s} d(x, z) \leq d(x, y) + \inf_{z \in s} d(y, z). \]

EMetric.edist_le_infEdist_add_ediam theorem

(hy : y ∈ s) : edist x y ≤ infEdist x s + diam s

Full source

theorem edist_le_infEdist_add_ediam (hy : y ∈ s) : edist x y ≤ infEdist x s + diam s := by
  simp_rw [infEdist, ENNReal.iInf_add]
  refine le_iInf₂ fun i hi => ?_
  calc
    edist x y ≤ edist x i + edist i y := edist_triangle _ _ _
    _ ≤ edist x i + diam s := add_le_add le_rfl (edist_le_diam_of_mem hi hy)

Extended Distance Bound via Infimal Distance and Diameter

Informal description

For any point $x$ in an extended metric space and any point $y$ in a subset $s$ of the space, the extended distance between $x$ and $y$ is bounded above by the sum of the minimal extended distance from $x$ to $s$ and the extended diameter of $s$, i.e., \[ d(x, y) \leq \inf_{z \in s} d(x, z) + \mathrm{diam}(s). \]

EMetric.continuous_infEdist theorem

: Continuous fun x => infEdist x s

Full source

/-- The edist to a set depends continuously on the point -/
@[continuity]
theorem continuous_infEdist : Continuous fun x => infEdist x s :=
  continuous_of_le_add_edist 1 (by simp) <| by
    simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]

Continuity of Minimal Extended Distance Function

Informal description

The function that maps a point $x$ in an extended metric space to its minimal extended distance $\inf_{y \in s} d(x, y)$ from a subset $s$ is continuous.

EMetric.infEdist_closure theorem

: infEdist x (closure s) = infEdist x s

Full source

/-- The edist to a set and to its closure coincide -/
theorem infEdist_closure : infEdist x (closure s) = infEdist x s := by
  refine le_antisymm (infEdist_anti subset_closure) ?_
  refine ENNReal.le_of_forall_pos_le_add fun ε εpos h => ?_
  have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos
  have : infEdist x (closure s) < infEdist x (closure s) + ε / 2 :=
    ENNReal.lt_add_right h.ne ε0.ne'
  obtain ⟨y : α, ycs : y ∈ closure s, hy : edist x y < infEdist x (closure s) + ↑ε / 2⟩ :=
    infEdist_lt_iff.mp this
  obtain ⟨z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2⟩ := EMetric.mem_closure_iff.1 ycs (ε / 2) ε0
  calc
    infEdist x s ≤ edist x z := infEdist_le_edist_of_mem zs
    _ ≤ edist x y + edist y z := edist_triangle _ _ _
    _ ≤ infEdist x (closure s) + ε / 2 + ε / 2 := add_le_add (le_of_lt hy) (le_of_lt dyz)
    _ = infEdist x (closure s) + ↑ε := by rw [add_assoc, ENNReal.add_halves]

Minimal Extended Distance to Set Equals Minimal Distance to its Closure

Informal description

For any point $x$ in an extended metric space and any subset $s$ of the space, the minimal extended distance from $x$ to the closure of $s$ is equal to the minimal extended distance from $x$ to $s$ itself, i.e., \[ \inf_{y \in \overline{s}} d(x, y) = \inf_{y \in s} d(x, y). \]

EMetric.mem_closure_iff_infEdist_zero theorem

: x ∈ closure s ↔ infEdist x s = 0

Full source

/-- A point belongs to the closure of `s` iff its infimum edistance to this set vanishes -/
theorem mem_closure_iff_infEdist_zero : x ∈ closure sx ∈ closure s ↔ infEdist x s = 0 :=
  ⟨fun h => by
    rw [← infEdist_closure]
    exact infEdist_zero_of_mem h,
   fun h =>
    EMetric.mem_closure_iff.2 fun ε εpos => infEdist_lt_iff.mp <| by rwa [h]⟩

Characterization of Closure via Zero Minimal Distance

Informal description

A point $x$ belongs to the closure of a set $s$ in an extended metric space if and only if the minimal extended distance from $x$ to $s$ is zero, i.e., \[ x \in \overline{s} \leftrightarrow \inf_{y \in s} d(x, y) = 0. \]

EMetric.mem_iff_infEdist_zero_of_closed theorem

(h : IsClosed s) : x ∈ s ↔ infEdist x s = 0

Full source

/-- Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes -/
theorem mem_iff_infEdist_zero_of_closed (h : IsClosed s) : x ∈ sx ∈ s ↔ infEdist x s = 0 := by
  rw [← mem_closure_iff_infEdist_zero, h.closure_eq]

Characterization of Membership in Closed Sets via Zero Minimal Distance

Informal description

For a closed subset $s$ of an extended metric space and a point $x$ in the space, $x$ belongs to $s$ if and only if the minimal extended distance from $x$ to $s$ is zero, i.e., \[ x \in s \leftrightarrow \inf_{y \in s} d(x, y) = 0. \]

EMetric.infEdist_pos_iff_not_mem_closure theorem

{x : α} {E : Set α} : 0 < infEdist x E ↔ x ∉ closure E

Full source

/-- The infimum edistance of a point to a set is positive if and only if the point is not in the
closure of the set. -/
theorem infEdist_pos_iff_not_mem_closure {x : α} {E : Set α} :
    0 < infEdist x E ↔ x ∉ closure E := by
  rw [mem_closure_iff_infEdist_zero, pos_iff_ne_zero]

Positivity of Minimal Distance Characterizes Non-Membership in Closure

Informal description

For a point $x$ in an extended metric space and a subset $E$ of the space, the minimal extended distance from $x$ to $E$ is positive if and only if $x$ does not belong to the closure of $E$, i.e., \[ \inf_{y \in E} d(x, y) > 0 \leftrightarrow x \notin \overline{E}. \]

EMetric.infEdist_closure_pos_iff_not_mem_closure theorem

{x : α} {E : Set α} : 0 < infEdist x (closure E) ↔ x ∉ closure E

Full source

theorem infEdist_closure_pos_iff_not_mem_closure {x : α} {E : Set α} :
    0 < infEdist x (closure E) ↔ x ∉ closure E := by
  rw [infEdist_closure, infEdist_pos_iff_not_mem_closure]

Positivity of Minimal Distance to Closure Characterizes Non-Membership in Closure

Informal description

For a point $x$ in an extended metric space and a subset $E$ of the space, the minimal extended distance from $x$ to the closure of $E$ is positive if and only if $x$ does not belong to the closure of $E$, i.e., \[ \inf_{y \in \overline{E}} d(x, y) > 0 \leftrightarrow x \notin \overline{E}. \]

EMetric.exists_real_pos_lt_infEdist_of_not_mem_closure theorem

{x : α} {E : Set α} (h : x ∉ closure E) : ∃ ε : ℝ, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Full source

theorem exists_real_pos_lt_infEdist_of_not_mem_closure {x : α} {E : Set α} (h : x ∉ closure E) :
    ∃ ε : ℝ, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E := by
  rw [← infEdist_pos_iff_not_mem_closure, ENNReal.lt_iff_exists_real_btwn] at h
  rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩
  exact ⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩

Existence of Positive Real Bound Below Minimal Distance for Points Outside Closure

Informal description

For any point $x$ in an extended metric space and any subset $E$ of the space, if $x$ does not belong to the closure of $E$, then there exists a positive real number $\varepsilon > 0$ such that the extended nonnegative real number obtained from $\varepsilon$ is strictly less than the minimal extended distance from $x$ to $E$, i.e., \[ \exists \varepsilon > 0, \quad \text{ofReal}(\varepsilon) < \inf_{y \in E} d(x, y). \]

EMetric.disjoint_closedBall_of_lt_infEdist theorem

{r : ℝ≥0∞} (h : r < infEdist x s) : Disjoint (closedBall x r) s

Full source

theorem disjoint_closedBall_of_lt_infEdist {r : ℝ≥0∞} (h : r < infEdist x s) :
    Disjoint (closedBall x r) s := by
  rw [disjoint_left]
  intro y hy h'y
  apply lt_irrefl (infEdist x s)
  calc
    infEdist x s ≤ edist x y := infEdist_le_edist_of_mem h'y
    _ ≤ r := by rwa [mem_closedBall, edist_comm] at hy
    _ < infEdist x s := h

Disjointness of Closed Ball and Set When Radius Less Than Minimal Distance

Informal description

For any extended nonnegative real number $r$ such that $r$ is strictly less than the minimal extended distance from a point $x$ to a set $s$ in an extended metric space, the closed ball centered at $x$ with radius $r$ is disjoint from $s$. In other words, if $r < \inf_{y \in s} d(x, y)$, then $\overline{B}(x, r) \cap s = \emptyset$.

EMetric.infEdist_image theorem

(hΦ : Isometry Φ) : infEdist (Φ x) (Φ '' t) = infEdist x t

Full source

/-- The infimum edistance is invariant under isometries -/
theorem infEdist_image (hΦ : Isometry Φ) : infEdist (Φ x) (Φ '' t) = infEdist x t := by
  simp only [infEdist, iInf_image, hΦ.edist_eq]

Isometry Invariance of Minimal Extended Distance

Informal description

Let $\Phi$ be an isometry between extended metric spaces. For any point $x$ and subset $t$ in the domain of $\Phi$, the minimal extended distance from $\Phi(x)$ to the image $\Phi(t)$ equals the minimal extended distance from $x$ to $t$, i.e., \[ \inf_{y \in t} d(\Phi(x), \Phi(y)) = \inf_{y \in t} d(x, y). \]

EMetric.infEdist_smul theorem

{M} [SMul M α] [IsIsometricSMul M α] (c : M) (x : α) (s : Set α) : infEdist (c • x) (c • s) = infEdist x s

Full source

@[to_additive (attr := simp)]
theorem infEdist_smul {M} [SMul M α] [IsIsometricSMul M α] (c : M) (x : α) (s : Set α) :
    infEdist (c • x) (c • s) = infEdist x s :=
  infEdist_image (isometry_smul _ _)

Minimal Extended Distance is Invariant under Isometric Scalar Multiplication

Informal description

Let $M$ be a type equipped with a scalar multiplication action on an extended metric space $\alpha$, and assume this action is isometric. For any scalar $c \in M$, point $x \in \alpha$, and subset $s \subseteq \alpha$, the minimal extended distance from $c \cdot x$ to the scaled set $c \cdot s$ equals the minimal extended distance from $x$ to $s$, i.e., \[ \inf_{y \in s} d(c \cdot x, c \cdot y) = \inf_{y \in s} d(x, y). \]

IsOpen.exists_iUnion_isClosed theorem

 {U : Set α} (hU : IsOpen U) : ∃ F : ℕ → Set α, (∀ n, IsClosed (F n)) ∧ (∀ n, F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F

Full source

theorem _root_.IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) :
    ∃ F : ℕ → Set α, (∀ n, IsClosed (F n)) ∧ (∀ n, F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F := by
  obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
  let F := fun n : ℕ => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
  have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
    by_contra h
    have : infEdistinfEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
    exact this (infEdist_zero_of_mem h)
  refine ⟨F, fun n => IsClosed.preimage continuous_infEdist isClosed_Ici, F_subset, ?_, ?_⟩
  · show ⋃ n, F n = U
    refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
    have : ¬x ∈ Uᶜ := by simpa using hx
    rw [mem_iff_infEdist_zero_of_closed hU.isClosed_compl] at this
    have B : 0 < infEdist x Uᶜ := by simpa [pos_iff_ne_zero] using this
    have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
      ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one
    rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
    simp only [mem_iUnion, mem_Ici, mem_preimage]
    exact ⟨n, hn.le⟩
  show Monotone F
  intro m n hmn x hx
  simp only [F, mem_Ici, mem_preimage] at hx ⊢
  apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx

Open Sets as Increasing Union of Closed Subsets

Informal description

For any open set $U$ in a topological space $\alpha$, there exists a sequence of closed subsets $(F_n)_{n \in \mathbb{N}}$ such that: 1. Each $F_n$ is closed, 2. $F_n \subseteq U$ for all $n$, 3. $\bigcup_{n \in \mathbb{N}} F_n = U$, 4. The sequence $(F_n)$ is monotone increasing (i.e., $F_n \subseteq F_{n+1}$ for all $n$).

IsCompact.exists_infEdist_eq_edist theorem

(hs : IsCompact s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, infEdist x s = edist x y

Full source

theorem _root_.IsCompact.exists_infEdist_eq_edist (hs : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infEdist x s = edist x y := by
  have A : Continuous fun y => edist x y := continuous_const.edist continuous_id
  obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn
  exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩

Existence of a Point Attaining Minimal Extended Distance to a Compact Set

Informal description

Let $s$ be a nonempty compact subset of an extended metric space $\alpha$, and let $x$ be a point in $\alpha$. Then there exists a point $y \in s$ such that the minimal extended distance from $x$ to $s$ is equal to the extended distance from $x$ to $y$, i.e., \[ \inf_{z \in s} d(x, z) = d(x, y). \]

EMetric.exists_pos_forall_lt_edist theorem

 (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) : ∃ r : ℝ≥0, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (r : ℝ≥0∞) < edist x y

Full source

theorem exists_pos_forall_lt_edist (hs : IsCompact s) (ht : IsClosed t) (hst : Disjoint s t) :
    ∃ r : ℝ≥0, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, (r : ℝ≥0∞) < edist x y := by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · use 1
    simp
  obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEdist.continuousOn
  have : 0 < infEdist x t :=
    pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEdist_zero_of_closed ht).mpr H⟩
  rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩
  exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h hy) z hz⟩

Positive separation distance between compact and closed disjoint sets in extended metric spaces

Informal description

Let $s$ and $t$ be subsets of an extended metric space such that $s$ is compact, $t$ is closed, and $s$ and $t$ are disjoint. Then there exists a positive real number $r > 0$ such that for all $x \in s$ and $y \in t$, the extended distance $d(x, y) > r$.

EMetric.hausdorffEdist definition

Full source

/-- The Hausdorff edistance between two sets is the smallest `r` such that each set
is contained in the `r`-neighborhood of the other one -/
irreducible_def hausdorffEdist {α : Type u} [PseudoEMetricSpace α] (s t : Set α) : ℝ≥0∞ :=
  (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s

Hausdorff extended distance between sets in a pseudoemetric space

Informal description

Given two subsets $s$ and $t$ of a pseudoemetric space $\alpha$, the Hausdorff extended distance between them is defined as the smallest extended nonnegative real number $r$ such that each set is contained in the $r$-neighborhood of the other. Formally, it is given by: \[ \text{hausdorffEdist}(s, t) = \left( \sup_{x \in s} \text{infEdist}(x, t) \right) \sqcup \left( \sup_{y \in t} \text{infEdist}(y, s) \right) \] where $\text{infEdist}(x, t)$ denotes the infimum of the extended distances from $x$ to points in $t$, and $\sqcup$ denotes the supremum operation in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EMetric.hausdorffEdist_def theorem

: eta_helper Eq✝ @hausdorffEdist.{} @(delta% @definition✝)

Full source

/-- The Hausdorff edistance between two sets is the smallest `r` such that each set
is contained in the `r`-neighborhood of the other one -/
irreducible_def hausdorffEdist {α : Type u} [PseudoEMetricSpace α] (s t : Set α) : ℝ≥0∞ :=
  (⨆ x ∈ s, infEdist x t) ⊔ ⨆ y ∈ t, infEdist y s

Definition of Hausdorff Extended Distance Between Sets

Informal description

The Hausdorff extended distance between two subsets $s$ and $t$ in a pseudoemetric space is defined as: \[ \text{hausdorffEdist}(s, t) = \max\left(\sup_{x \in s} \inf_{y \in t} d(x, y), \sup_{y \in t} \inf_{x \in s} d(x, y)\right) \] where $d(x,y)$ denotes the extended distance between points $x$ and $y$ in the space.

EMetric.hausdorffEdist_self theorem

: hausdorffEdist s s = 0

Full source

/-- The Hausdorff edistance of a set to itself vanishes. -/
@[simp]
theorem hausdorffEdist_self : hausdorffEdist s s = 0 := by
  simp only [hausdorffEdist_def, sup_idem, ENNReal.iSup_eq_zero]
  exact fun x hx => infEdist_zero_of_mem hx

Hausdorff Distance of a Set to Itself Vanishes

Informal description

For any subset $s$ of an extended metric space, the Hausdorff extended distance between $s$ and itself is zero, i.e., \[ \text{hausdorffEdist}(s, s) = 0. \]

EMetric.hausdorffEdist_comm theorem

: hausdorffEdist s t = hausdorffEdist t s

Full source

/-- The Haudorff edistances of `s` to `t` and of `t` to `s` coincide. -/
theorem hausdorffEdist_comm : hausdorffEdist s t = hausdorffEdist t s := by
  simp only [hausdorffEdist_def]; apply sup_comm

Symmetry of Hausdorff Extended Distance

Informal description

For any two subsets $s$ and $t$ of an extended metric space, the Hausdorff extended distance from $s$ to $t$ is equal to the Hausdorff extended distance from $t$ to $s$, i.e., \[ \text{hausdorffEdist}(s, t) = \text{hausdorffEdist}(t, s). \]

EMetric.hausdorffEdist_le_of_infEdist theorem

 {r : ℝ≥0∞} (H1 : ∀ x ∈ s, infEdist x t ≤ r) (H2 : ∀ x ∈ t, infEdist x s ≤ r) : hausdorffEdist s t ≤ r

Full source

/-- 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⟩

Upper Bound on Hausdorff Extended Distance via Pointwise Minimal Distances

Informal description

For any extended nonnegative real number $r$ and any two subsets $s$ and $t$ in an extended metric space, if for every point $x \in s$ the minimal extended distance from $x$ to $t$ is at most $r$, and similarly for every point $x \in t$ the minimal extended distance from $x$ to $s$ is at most $r$, then the Hausdorff extended distance between $s$ and $t$ is at most $r$.

EMetric.hausdorffEdist_le_of_mem_edist theorem

 {r : ℝ≥0∞} (H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) (H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) : hausdorffEdist s t ≤ r

Full source

/-- Bounding the Hausdorff edistance by exhibiting, for any point in each set,
another point in the other set at controlled distance -/
theorem hausdorffEdist_le_of_mem_edist {r : ℝ≥0∞} (H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r)
    (H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) : hausdorffEdist s t ≤ r := by
  refine hausdorffEdist_le_of_infEdist (fun x xs ↦ ?_) (fun x xt ↦ ?_)
  · rcases H1 x xs with ⟨y, yt, hy⟩
    exact le_trans (infEdist_le_edist_of_mem yt) hy
  · rcases H2 x xt with ⟨y, ys, hy⟩
    exact le_trans (infEdist_le_edist_of_mem ys) hy

Upper Bound on Hausdorff Distance via Pointwise Distance Control

Informal description

For any extended nonnegative real number $r$ and any two subsets $s$ and $t$ in an extended metric space, if for every point $x \in s$ there exists a point $y \in t$ such that the extended distance $d(x, y) \leq r$, and similarly for every point $x \in t$ there exists $y \in s$ with $d(x, y) \leq r$, then the Hausdorff extended distance between $s$ and $t$ satisfies $\text{hausdorffEdist}(s, t) \leq r$.

EMetric.infEdist_le_hausdorffEdist_of_mem theorem

(h : x ∈ s) : infEdist x t ≤ hausdorffEdist s t

Full source

/-- 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

Minimal Distance to a Set is Bounded by Hausdorff Distance

Informal description

For any point $x$ in a subset $s$ of an extended metric space, the minimal extended distance from $x$ to another subset $t$ is bounded above by the Hausdorff extended distance between $s$ and $t$, i.e., \[ \inf_{y \in t} d(x, y) \leq \text{hausdorffEdist}(s, t). \]

EMetric.exists_edist_lt_of_hausdorffEdist_lt theorem

{r : ℝ≥0∞} (h : x ∈ s) (H : hausdorffEdist s t < r) : ∃ y ∈ t, edist x y < r

Full source

/-- 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

Existence of Close Points under Hausdorff Distance Condition

Informal description

For any point $x$ in a subset $s$ of an extended metric space, if the Hausdorff extended distance between $s$ and another subset $t$ is less than some extended nonnegative real number $r$, then there exists a point $y \in t$ such that the extended distance between $x$ and $y$ is less than $r$, i.e., \[ \text{hausdorffEdist}(s, t) < r \implies \exists y \in t, d(x, y) < r. \]

EMetric.infEdist_le_infEdist_add_hausdorffEdist theorem

: infEdist x t ≤ infEdist x s + hausdorffEdist s t

Full source

/-- The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
between `s` and `t`. -/
theorem infEdist_le_infEdist_add_hausdorffEdist :
    infEdist x t ≤ infEdist x s + hausdorffEdist s t :=
  ENNReal.le_of_forall_pos_le_add fun ε εpos h => by
    have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos
    have : infEdist x s < infEdist x s + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0
    obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEdist x s + ↑ε / 2⟩ := infEdist_lt_iff.mp this
    have : hausdorffEdist s t < hausdorffEdist s t + ε / 2 :=
      ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0
    obtain ⟨z : α, zt : z ∈ t, dyz : edist y z < hausdorffEdist s t + ↑ε / 2⟩ :=
      exists_edist_lt_of_hausdorffEdist_lt ys this
    calc
      infEdist x t ≤ edist x z := infEdist_le_edist_of_mem zt
      _ ≤ edist x y + edist y z := edist_triangle _ _ _
      _ ≤ infEdist x s + ε / 2 + (hausdorffEdist s t + ε / 2) := add_le_add dxy.le dyz.le
      _ = infEdist x s + hausdorffEdist s t + ε := by
        simp [ENNReal.add_halves, add_comm, add_left_comm]

Triangle Inequality for Minimal Distance and Hausdorff Distance

Informal description

For any point $x$ in an extended metric space and any two subsets $s$ and $t$ of the space, the minimal extended distance from $x$ to $t$ is bounded above by the sum of the minimal extended distance from $x$ to $s$ and the Hausdorff extended distance between $s$ and $t$, i.e., \[ \inf_{y \in t} d(x, y) \leq \inf_{z \in s} d(x, z) + \text{hausdorffEdist}(s, t). \]

EMetric.hausdorffEdist_image theorem

(h : Isometry Φ) : hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t

Full source

/-- The Hausdorff edistance is invariant under isometries. -/
theorem hausdorffEdist_image (h : Isometry Φ) :
    hausdorffEdist (Φ '' s) (Φ '' t) = hausdorffEdist s t := by
  simp only [hausdorffEdist_def, iSup_image, infEdist_image h]

Isometry Invariance of Hausdorff Extended Distance

Informal description

Let $\Phi$ be an isometry between extended metric spaces. For any two subsets $s$ and $t$ in the domain of $\Phi$, the Hausdorff extended distance between the images $\Phi(s)$ and $\Phi(t)$ equals the Hausdorff extended distance between $s$ and $t$, i.e., \[ \text{hausdorffEdist}(\Phi(s), \Phi(t)) = \text{hausdorffEdist}(s, t). \]

EMetric.hausdorffEdist_le_ediam theorem

(hs : s.Nonempty) (ht : t.Nonempty) : hausdorffEdist s t ≤ diam (s ∪ t)

Full source

/-- The Hausdorff distance is controlled by the diameter of the union. -/
theorem hausdorffEdist_le_ediam (hs : s.Nonempty) (ht : t.Nonempty) :
    hausdorffEdist s t ≤ diam (s ∪ t) := by
  rcases hs with ⟨x, xs⟩
  rcases ht with ⟨y, yt⟩
  refine hausdorffEdist_le_of_mem_edist ?_ ?_
  · intro z hz
    exact ⟨y, yt, edist_le_diam_of_mem (subset_union_left hz) (subset_union_right yt)⟩
  · intro z hz
    exact ⟨x, xs, edist_le_diam_of_mem (subset_union_right hz) (subset_union_left xs)⟩

Hausdorff Distance Bounded by Union Diameter

Informal description

For any nonempty subsets $s$ and $t$ of an extended metric space, the Hausdorff extended distance between $s$ and $t$ is bounded above by the diameter of their union, i.e., \[ \text{hausdorffEdist}(s, t) \leq \text{diam}(s \cup t). \]

EMetric.hausdorffEdist_triangle theorem

: hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u

Full source

/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffEdist_triangle : hausdorffEdist s u ≤ hausdorffEdist s t + hausdorffEdist t u := by
  rw [hausdorffEdist_def]
  simp only [sup_le_iff, iSup_le_iff]
  constructor
  · show ∀ x ∈ s, infEdist x u ≤ hausdorffEdist s t + hausdorffEdist t u
    exact fun x xs =>
      calc
        infEdist x u ≤ infEdist x t + hausdorffEdist t u :=
          infEdist_le_infEdist_add_hausdorffEdist
        _ ≤ hausdorffEdist s t + hausdorffEdist t u :=
          add_le_add_right (infEdist_le_hausdorffEdist_of_mem xs) _
  · show ∀ x ∈ u, infEdist x s ≤ hausdorffEdist s t + hausdorffEdist t u
    exact fun x xu =>
      calc
        infEdist x s ≤ infEdist x t + hausdorffEdist t s :=
          infEdist_le_infEdist_add_hausdorffEdist
        _ ≤ hausdorffEdist u t + hausdorffEdist t s :=
          add_le_add_right (infEdist_le_hausdorffEdist_of_mem xu) _
        _ = hausdorffEdist s t + hausdorffEdist t u := by simp [hausdorffEdist_comm, add_comm]

Triangle Inequality for Hausdorff Extended Distance

Informal description

For any three subsets $s$, $t$, and $u$ of an extended metric space, the Hausdorff extended distance between $s$ and $u$ is bounded above by the sum of the Hausdorff extended distances between $s$ and $t$ and between $t$ and $u$, i.e., \[ \text{hausdorffEdist}(s, u) \leq \text{hausdorffEdist}(s, t) + \text{hausdorffEdist}(t, u). \]

EMetric.hausdorffEdist_zero_iff_closure_eq_closure theorem

: hausdorffEdist s t = 0 ↔ closure s = closure t

Full source

/-- Two sets are at zero Hausdorff edistance if and only if they have the same closure. -/
theorem hausdorffEdist_zero_iff_closure_eq_closure :
    hausdorffEdisthausdorffEdist s t = 0 ↔ closure s = closure t := by
  simp only [hausdorffEdist_def, ENNReal.sup_eq_zero, ENNReal.iSup_eq_zero, ← subset_def,
    ← mem_closure_iff_infEdist_zero, subset_antisymm_iff, isClosed_closure.closure_subset_iff]

Hausdorff Distance Zero Characterizes Equal Closures

Informal description

For any two subsets $s$ and $t$ of an extended metric space, the Hausdorff extended distance between them is zero if and only if their closures are equal, i.e., \[ \text{hausdorffEdist}(s, t) = 0 \leftrightarrow \overline{s} = \overline{t}. \]

EMetric.hausdorffEdist_self_closure theorem

: hausdorffEdist s (closure s) = 0

Full source

/-- The Hausdorff edistance between a set and its closure vanishes. -/
@[simp]
theorem hausdorffEdist_self_closure : hausdorffEdist s (closure s) = 0 := by
  rw [hausdorffEdist_zero_iff_closure_eq_closure, closure_closure]

Hausdorff Distance Between Set and Its Closure Vanishes

Informal description

For any subset $s$ of an extended metric space, the Hausdorff extended distance between $s$ and its closure $\overline{s}$ is zero, i.e., \[ \text{hausdorffEdist}(s, \overline{s}) = 0. \]

EMetric.hausdorffEdist_closure₁ theorem

: hausdorffEdist (closure s) t = hausdorffEdist s t

Full source

/-- Replacing a set by its closure does not change the Hausdorff edistance. -/
@[simp]
theorem hausdorffEdist_closure₁ : hausdorffEdist (closure s) t = hausdorffEdist s t := by
  refine le_antisymm ?_ ?_
  · calc
      _ ≤ hausdorffEdist (closure s) s + hausdorffEdist s t := hausdorffEdist_triangle
      _ = hausdorffEdist s t := by simp [hausdorffEdist_comm]
  · calc
      _ ≤ hausdorffEdist s (closure s) + hausdorffEdist (closure s) t := hausdorffEdist_triangle
      _ = hausdorffEdist (closure s) t := by simp

Hausdorff Distance Invariance Under Closure of First Set

Informal description

For any subset $s$ and any subset $t$ of an extended metric space, the Hausdorff extended distance between the closure of $s$ and $t$ is equal to the Hausdorff extended distance between $s$ and $t$, i.e., \[ \text{hausdorffEdist}(\overline{s}, t) = \text{hausdorffEdist}(s, t). \]

EMetric.hausdorffEdist_closure₂ theorem

: hausdorffEdist s (closure t) = hausdorffEdist s t

Full source

/-- Replacing a set by its closure does not change the Hausdorff edistance. -/
@[simp]
theorem hausdorffEdist_closure₂ : hausdorffEdist s (closure t) = hausdorffEdist s t := by
  simp [@hausdorffEdist_comm _ _ s _]

Hausdorff Distance Invariance Under Closure of Second Set

Informal description

For any subsets $s$ and $t$ of an extended metric space, the Hausdorff extended distance between $s$ and the closure of $t$ is equal to the Hausdorff extended distance between $s$ and $t$, i.e., \[ \text{hausdorffEdist}(s, \overline{t}) = \text{hausdorffEdist}(s, t). \]

EMetric.hausdorffEdist_closure theorem

: hausdorffEdist (closure s) (closure t) = hausdorffEdist s t

Full source

/-- The Hausdorff edistance between sets or their closures is the same. -/
theorem hausdorffEdist_closure : hausdorffEdist (closure s) (closure t) = hausdorffEdist s t := by
  simp

Hausdorff Distance Invariance Under Closure

Informal description

For any subsets $s$ and $t$ of an extended metric space, the Hausdorff extended distance between their closures is equal to the Hausdorff extended distance between $s$ and $t$, i.e., \[ \text{hausdorffEdist}(\overline{s}, \overline{t}) = \text{hausdorffEdist}(s, t). \]

EMetric.hausdorffEdist_zero_iff_eq_of_closed theorem

(hs : IsClosed s) (ht : IsClosed t) : hausdorffEdist s t = 0 ↔ s = t

Full source

/-- Two closed sets are at zero Hausdorff edistance if and only if they coincide. -/
theorem hausdorffEdist_zero_iff_eq_of_closed (hs : IsClosed s) (ht : IsClosed t) :
    hausdorffEdisthausdorffEdist s t = 0 ↔ s = t := by
  rw [hausdorffEdist_zero_iff_closure_eq_closure, hs.closure_eq, ht.closure_eq]

Hausdorff Distance Zero Characterizes Equality for Closed Sets

Informal description

For any two closed subsets $s$ and $t$ in an extended metric space, the Hausdorff extended distance between them is zero if and only if the sets are equal, i.e., \[ \text{hausdorffEdist}(s, t) = 0 \leftrightarrow s = t. \]

EMetric.hausdorffEdist_empty theorem

(ne : s.Nonempty) : hausdorffEdist s ∅ = ∞

Full source

/-- The Haudorff edistance to the empty set is infinite. -/
theorem hausdorffEdist_empty (ne : s.Nonempty) : hausdorffEdist s ∅ = ∞ := by
  rcases ne with ⟨x, xs⟩
  have : infEdist x ∅ ≤ hausdorffEdist s ∅ := infEdist_le_hausdorffEdist_of_mem xs
  simpa using this

Hausdorff Distance to Empty Set is Infinite for Nonempty Sets

Informal description

For any nonempty subset $s$ of an extended metric space, the Hausdorff extended distance between $s$ and the empty set is $\infty$.

EMetric.nonempty_of_hausdorffEdist_ne_top theorem

(hs : s.Nonempty) (fin : hausdorffEdist s t ≠ ⊤) : t.Nonempty

Full source

/-- If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty. -/
theorem nonempty_of_hausdorffEdist_ne_top (hs : s.Nonempty) (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) :
    t.Nonempty :=
  t.eq_empty_or_nonempty.resolve_left fun ht ↦ fin (ht.symm ▸ hausdorffEdist_empty hs)

Nonemptiness of Second Set under Finite Hausdorff Distance

Informal description

Let $s$ and $t$ be subsets of an extended metric space. If $s$ is nonempty and the Hausdorff extended distance between $s$ and $t$ is finite, then $t$ is also nonempty.

EMetric.empty_or_nonempty_of_hausdorffEdist_ne_top theorem

(fin : hausdorffEdist s t ≠ ⊤) : (s = ∅ ∧ t = ∅) ∨ (s.Nonempty ∧ t.Nonempty)

Full source

theorem empty_or_nonempty_of_hausdorffEdist_ne_top (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) :
    (s = ∅ ∧ t = ∅) ∨ (s.Nonempty ∧ t.Nonempty) := by
  rcases s.eq_empty_or_nonempty with hs | hs
  · rcases t.eq_empty_or_nonempty with ht | ht
    · exact Or.inl ⟨hs, ht⟩
    · rw [hausdorffEdist_comm] at fin
      exact Or.inr ⟨nonempty_of_hausdorffEdist_ne_top ht fin, ht⟩
  · exact Or.inr ⟨hs, nonempty_of_hausdorffEdist_ne_top hs fin⟩

Finite Hausdorff Distance Implies Both Sets Empty or Both Nonempty

Informal description

For any two subsets $s$ and $t$ of an extended metric space, if their Hausdorff extended distance is finite, then either both sets are empty or both sets are nonempty. In other words, $\text{hausdorffEdist}(s, t) \neq \infty$ implies $(s = \emptyset \land t = \emptyset) \lor (s \neq \emptyset \land t \neq \emptyset)$.

Metric.infDist definition

(x : α) (s : Set α) : ℝ

Full source

/-- The minimal distance of a point to a set -/
def infDist (x : α) (s : Set α) : ℝ :=
  ENNReal.toReal (infEdist x s)

Minimal distance from a point to a set

Informal description

Given a point $x$ in a metric space $\alpha$ and a subset $s \subseteq \alpha$, the minimal distance from $x$ to $s$ is defined as the infimum of the distances from $x$ to all points $y$ in $s$, converted to a real number. If the infimum is infinite (i.e., when $s$ is empty), the result is $0$.

Metric.infDist_eq_iInf theorem

: infDist x s = ⨅ y : s, dist x y

Full source

theorem infDist_eq_iInf : infDist x s = ⨅ y : s, dist x y := by
  rw [infDist, infEdist, iInf_subtype', ENNReal.toReal_iInf]
  · simp only [dist_edist]
  · exact fun _ ↦ edist_ne_top _ _

Minimal Distance Equals Infimum of Pointwise Distances

Informal description

For any point $x$ in a metric space $\alpha$ and any subset $s \subseteq \alpha$, the minimal distance from $x$ to $s$ is equal to the infimum of the distances from $x$ to all points $y$ in $s$, i.e., \[ \text{infDist}(x, s) = \inf_{y \in s} \text{dist}(x, y). \]

Metric.infDist_nonneg theorem

: 0 ≤ infDist x s

Full source

/-- The minimal distance is always nonnegative -/
theorem infDist_nonneg : 0 ≤ infDist x s := toReal_nonneg

Nonnegativity of Minimal Distance to a Set

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the minimal distance from $x$ to $s$ is nonnegative, i.e., $\inf_{y \in s} d(x, y) \geq 0$.

Metric.infDist_empty theorem

: infDist x ∅ = 0

Full source

/-- The minimal distance to the empty set is 0 (if you want to have the more reasonable
value `∞` instead, use `EMetric.infEdist`, which takes values in `ℝ≥0∞`) -/
@[simp]
theorem infDist_empty : infDist x ∅ = 0 := by simp [infDist]

Minimal Distance to Empty Set is Zero

Informal description

For any point $x$ in a metric space, the minimal distance from $x$ to the empty set is $0$.

Metric.isGLB_infDist theorem

(hs : s.Nonempty) : IsGLB ((dist x ·) '' s) (infDist x s)

Full source

lemma isGLB_infDist (hs : s.Nonempty) : IsGLB ((dist x ·) '' s) (infDist x s) := by
  simpa [infDist_eq_iInf, sInf_image']
    using isGLB_csInf (hs.image _) ⟨0, by simp [lowerBounds, dist_nonneg]⟩

Minimal Distance to Set is Greatest Lower Bound of Pointwise Distances

Informal description

For any nonempty subset $s$ of a pseudometric space and any point $x$ in the space, the minimal distance $\text{infDist}(x, s)$ is the greatest lower bound of the set of distances $\{d(x,y) \mid y \in s\}$.

Metric.infEdist_ne_top theorem

(h : s.Nonempty) : infEdist x s ≠ ⊤

Full source

/-- In a metric space, the minimal edistance to a nonempty set is finite. -/
theorem infEdist_ne_top (h : s.Nonempty) : infEdistinfEdist x s ≠ ⊤ := by
  rcases h with ⟨y, hy⟩
  exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEdist_le_edist_of_mem hy)

Finiteness of Minimal Extended Distance to Nonempty Sets in Pseudometric Spaces

Informal description

In a pseudometric space, for any nonempty subset $s$ and any point $x$, the minimal extended distance from $x$ to $s$ is finite, i.e., $\inf_{y \in s} d(x, y) \neq \infty$.

Metric.infEdist_eq_top_iff theorem

: infEdist x s = ∞ ↔ s = ∅

Full source

@[simp]
theorem infEdist_eq_top_iff : infEdistinfEdist x s = ∞ ↔ s = ∅ := by
  rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [*, Nonempty.ne_empty, infEdist_ne_top]

Minimal Extended Distance to Set is Infinite if and only if Set is Empty

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the minimal extended distance from $x$ to $s$ is infinite if and only if $s$ is the empty set, i.e., \[ \inf_{y \in s} d(x, y) = \infty \leftrightarrow s = \emptyset. \]

Metric.infDist_zero_of_mem theorem

(h : x ∈ s) : infDist x s = 0

Full source

/-- The minimal distance of a point to a set containing it vanishes. -/
theorem infDist_zero_of_mem (h : x ∈ s) : infDist x s = 0 := by
  simp [infEdist_zero_of_mem h, infDist]

Minimal Distance to Set is Zero for Points in the Set

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, if $x$ belongs to $s$, then the minimal distance from $x$ to $s$ is zero, i.e., \[ \inf_{y \in s} d(x, y) = 0. \]

Metric.infDist_singleton theorem

: infDist x { y } = dist x y

Full source

/-- The minimal distance to a singleton is the distance to the unique point in this singleton. -/
@[simp]
theorem infDist_singleton : infDist x {y} = dist x y := by simp [infDist, dist_edist]

Minimal Distance to Singleton Equals Point Distance

Informal description

For any point $x$ in a pseudometric space and any singleton set $\{y\}$, the minimal distance from $x$ to $\{y\}$ is equal to the distance between $x$ and $y$, i.e., \[ \inf_{z \in \{y\}} d(x, z) = d(x, y). \]

Metric.infDist_le_dist_of_mem theorem

(h : y ∈ s) : infDist x s ≤ dist x y

Full source

/-- The minimal distance to a set is bounded by the distance to any point in this set. -/
theorem infDist_le_dist_of_mem (h : y ∈ s) : infDist x s ≤ dist x y := by
  rw [dist_edist, infDist]
  exact ENNReal.toReal_mono (edist_ne_top _ _) (infEdist_le_edist_of_mem h)

Minimal Distance to Set is Bounded by Distance to Any Point in the Set

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any subset $s \subseteq \alpha$, if $y \in s$, then the minimal distance from $x$ to $s$ is less than or equal to the distance from $x$ to $y$, i.e., \[ \inf_{z \in s} d(x, z) \leq d(x, y). \]

Metric.infDist_le_infDist_of_subset theorem

(h : s ⊆ t) (hs : s.Nonempty) : infDist x t ≤ infDist x s

Full source

/-- The minimal distance is monotone with respect to inclusion. -/
theorem infDist_le_infDist_of_subset (h : s ⊆ t) (hs : s.Nonempty) : infDist x t ≤ infDist x s :=
  ENNReal.toReal_mono (infEdist_ne_top hs) (infEdist_anti h)

Monotonicity of Minimal Distance with Respect to Set Inclusion

Informal description

For any nonempty subset $s$ of a pseudometric space $\alpha$ and any subset $t$ containing $s$ (i.e., $s \subseteq t$), the minimal distance from a point $x$ to $t$ is less than or equal to the minimal distance from $x$ to $s$, i.e., \[ \inf_{y \in t} d(x, y) \leq \inf_{y \in s} d(x, y). \]

Metric.le_infDist theorem

{r : ℝ} (hs : s.Nonempty) : r ≤ infDist x s ↔ ∀ ⦃y⦄, y ∈ s → r ≤ dist x y

Full source

lemma le_infDist {r : ℝ} (hs : s.Nonempty) : r ≤ infDist x s ↔ ∀ ⦃y⦄, y ∈ s → r ≤ dist x y := by
  simp_rw [infDist, ← ENNReal.ofReal_le_iff_le_toReal (infEdist_ne_top hs), le_infEdist,
    ENNReal.ofReal_le_iff_le_toReal (edist_ne_top _ _), ← dist_edist]

Characterization of Infimal Distance via Pointwise Inequality

Informal description

For any real number $r$ and nonempty subset $s$ of a metric space, $r$ is less than or equal to the infimal distance from a point $x$ to $s$ if and only if for every point $y$ in $s$, $r$ is less than or equal to the distance between $x$ and $y$. In other words: $$ r \leq \inf_{y \in s} d(x, y) \iff \forall y \in s, r \leq d(x, y). $$

Metric.infDist_lt_iff theorem

{r : ℝ} (hs : s.Nonempty) : infDist x s < r ↔ ∃ y ∈ s, dist x y < r

Full source

/-- The minimal distance to a set `s` is `< r` iff there exists a point in `s` at distance `< r`. -/
theorem infDist_lt_iff {r : ℝ} (hs : s.Nonempty) : infDistinfDist x s < r ↔ ∃ y ∈ s, dist x y < r := by
  simp [← not_le, le_infDist hs]

Characterization of Infimal Distance via Strict Inequality

Informal description

For any real number $r$ and nonempty subset $s$ of a pseudometric space, the infimal distance from a point $x$ to $s$ is less than $r$ if and only if there exists a point $y \in s$ such that the distance between $x$ and $y$ is less than $r$. In other words: $$ \inf_{y \in s} d(x, y) < r \iff \exists y \in s, d(x, y) < r. $$

Metric.infDist_le_infDist_add_dist theorem

: infDist x s ≤ infDist y s + dist x y

Full source

/-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
the distance between `x` and `y`. -/
theorem infDist_le_infDist_add_dist : infDist x s ≤ infDist y s + dist x y := by
  rw [infDist, infDist, dist_edist]
  refine ENNReal.toReal_le_add' infEdist_le_infEdist_add_edist ?_ (flip absurd (edist_ne_top _ _))
  simp only [infEdist_eq_top_iff, imp_self]

Triangle Inequality for Minimal Distance: $\inf_{z \in s} d(x, z) \leq \inf_{z \in s} d(y, z) + d(x, y)$

Informal description

For any points $x$ and $y$ in a pseudometric space and any subset $s$ of the space, the minimal distance from $x$ to $s$ is bounded above by the sum of the minimal distance from $y$ to $s$ and the distance between $x$ and $y$, i.e., \[ \inf_{z \in s} d(x, z) \leq \inf_{z \in s} d(y, z) + d(x, y). \]

Metric.not_mem_of_dist_lt_infDist theorem

(h : dist x y < infDist x s) : y ∉ s

Full source

theorem not_mem_of_dist_lt_infDist (h : dist x y < infDist x s) : y ∉ s := fun hy =>
  h.not_le <| infDist_le_dist_of_mem hy

Non-membership Criterion via Distance Comparison: $d(x,y) < \inf_{z \in s} d(x,z) \implies y \notin s$

Informal description

For any points $x$ and $y$ in a pseudometric space and any subset $s$ of the space, if the distance between $x$ and $y$ is strictly less than the minimal distance from $x$ to $s$, then $y$ does not belong to $s$. In other words, if $d(x, y) < \inf_{z \in s} d(x, z)$, then $y \notin s$.

Metric.disjoint_ball_infDist theorem

: Disjoint (ball x (infDist x s)) s

Full source

theorem disjoint_ball_infDist : Disjoint (ball x (infDist x s)) s :=
  disjoint_left.2 fun _y hy => not_mem_of_dist_lt_infDist <| mem_ball'.1 hy

Disjointness of Minimal Distance Ball and Set

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the open ball centered at $x$ with radius equal to the minimal distance from $x$ to $s$ is disjoint from $s$. That is, $\text{ball}(x, \inf_{y \in s} d(x, y)) \cap s = \emptyset$.

Metric.ball_infDist_subset_compl theorem

: ball x (infDist x s) ⊆ sᶜ

Full source

theorem ball_infDist_subset_compl : ballball x (infDist x s) ⊆ sᶜ :=
  (disjoint_ball_infDist (s := s)).subset_compl_right

Open Ball of Minimal Distance is Contained in Complement of Set

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the open ball centered at $x$ with radius equal to the minimal distance from $x$ to $s$ is contained in the complement of $s$. That is, $\text{ball}(x, \inf_{y \in s} d(x, y)) \subseteq s^c$.

Metric.ball_infDist_compl_subset theorem

: ball x (infDist x sᶜ) ⊆ s

Full source

theorem ball_infDist_compl_subset : ballball x (infDist x sᶜ) ⊆ s :=
  ball_infDist_subset_compl.trans_eq (compl_compl s)

Open Ball of Minimal Distance to Complement is Contained in Set

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the open ball centered at $x$ with radius equal to the minimal distance from $x$ to the complement of $s$ is contained in $s$. That is, $\text{ball}(x, \inf_{y \notin s} d(x, y)) \subseteq s$.

Metric.disjoint_closedBall_of_lt_infDist theorem

{r : ℝ} (h : r < infDist x s) : Disjoint (closedBall x r) s

Full source

theorem disjoint_closedBall_of_lt_infDist {r : ℝ} (h : r < infDist x s) :
    Disjoint (closedBall x r) s :=
  disjoint_ball_infDist.mono_left <| closedBall_subset_ball h

Disjointness of Closed Ball and Set for Radius Below Minimal Distance

Informal description

For any real number $r$ such that $r$ is less than the minimal distance from a point $x$ to a set $s$ in a pseudometric space, the closed ball centered at $x$ with radius $r$ is disjoint from $s$. That is, if $r < \inf_{y \in s} d(x, y)$, then $\overline{B}(x, r) \cap s = \emptyset$.

Metric.dist_le_infDist_add_diam theorem

(hs : IsBounded s) (hy : y ∈ s) : dist x y ≤ infDist x s + diam s

Full source

theorem dist_le_infDist_add_diam (hs : IsBounded s) (hy : y ∈ s) :
    dist x y ≤ infDist x s + diam s := by
  rw [infDist, diam, dist_edist]
  exact toReal_le_add (edist_le_infEdist_add_ediam hy) (infEdist_ne_top ⟨y, hy⟩) hs.ediam_ne_top

Distance Bound via Minimal Distance and Diameter in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any point $y$ in a bounded subset $s \subseteq \alpha$, the distance between $x$ and $y$ is bounded above by the sum of the minimal distance from $x$ to $s$ and the diameter of $s$, i.e., \[ d(x, y) \leq \inf_{z \in s} d(x, z) + \mathrm{diam}(s). \]

Metric.lipschitz_infDist_pt theorem

: LipschitzWith 1 (infDist · s)

Full source

/-- The minimal distance to a set is Lipschitz in point with constant 1 -/
theorem lipschitz_infDist_pt : LipschitzWith 1 (infDist · s) :=
  LipschitzWith.of_le_add fun _ _ => infDist_le_infDist_add_dist

Lipschitz continuity of minimal distance function with constant 1

Informal description

For any subset $s$ of a pseudometric space, the function $x \mapsto \inf_{y \in s} d(x, y)$ is Lipschitz continuous with constant $1$, where $d$ is the distance function of the space.

Metric.uniformContinuous_infDist_pt theorem

: UniformContinuous (infDist · s)

Full source

/-- The minimal distance to a set is uniformly continuous in point -/
theorem uniformContinuous_infDist_pt : UniformContinuous (infDist · s) :=
  (lipschitz_infDist_pt s).uniformContinuous

Uniform Continuity of Minimal Distance Function to a Set

Informal description

For any subset $s$ of a pseudometric space, the function $x \mapsto \inf_{y \in s} d(x, y)$, which measures the minimal distance from a point $x$ to the set $s$, is uniformly continuous.

Metric.continuous_infDist_pt theorem

: Continuous (infDist · s)

Full source

/-- The minimal distance to a set is continuous in point -/
@[continuity]
theorem continuous_infDist_pt : Continuous (infDist · s) :=
  (uniformContinuous_infDist_pt s).continuous

Continuity of Minimal Distance Function to a Set

Informal description

For any subset $s$ of a pseudometric space, the function $x \mapsto \inf_{y \in s} d(x,y)$, which gives the minimal distance from a point $x$ to the set $s$, is continuous.

Metric.infDist_closure theorem

: infDist x (closure s) = infDist x s

Full source

/-- The minimal distances to a set and its closure coincide. -/
theorem infDist_closure : infDist x (closure s) = infDist x s := by
  simp [infDist, infEdist_closure]

Minimal Distance to Set Equals Minimal Distance to its Closure

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, the minimal distance from $x$ to the closure of $s$ is equal to the minimal distance from $x$ to $s$ itself, i.e., \[ \inf_{y \in \overline{s}} d(x, y) = \inf_{y \in s} d(x, y). \]

Metric.infDist_zero_of_mem_closure theorem

(hx : x ∈ closure s) : infDist x s = 0

Full source

/-- If a point belongs to the closure of `s`, then its infimum distance to `s` equals zero.
The converse is true provided that `s` is nonempty, see `Metric.mem_closure_iff_infDist_zero`. -/
theorem infDist_zero_of_mem_closure (hx : x ∈ closure s) : infDist x s = 0 := by
  rw [← infDist_closure]
  exact infDist_zero_of_mem hx

Minimal Distance to Set is Zero for Points in its Closure

Informal description

For any point $x$ in a pseudometric space and any subset $s$ of the space, if $x$ belongs to the closure of $s$, then the minimal distance from $x$ to $s$ is zero, i.e., \[ \inf_{y \in s} d(x, y) = 0. \]

Metric.mem_closure_iff_infDist_zero theorem

(h : s.Nonempty) : x ∈ closure s ↔ infDist x s = 0

Full source

/-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes. -/
theorem mem_closure_iff_infDist_zero (h : s.Nonempty) : x ∈ closure sx ∈ closure s ↔ infDist x s = 0 := by
  simp [mem_closure_iff_infEdist_zero, infDist, ENNReal.toReal_eq_zero_iff, infEdist_ne_top h]

Characterization of Closure via Infimum Distance

Informal description

Let $s$ be a nonempty subset of a pseudometric space $\alpha$. A point $x \in \alpha$ belongs to the closure of $s$ if and only if the infimum distance from $x$ to $s$ is zero, i.e., \[ x \in \overline{s} \leftrightarrow \inf_{y \in s} d(x, y) = 0. \]

Metric.infDist_pos_iff_not_mem_closure theorem

(hs : s.Nonempty) : x ∉ closure s ↔ 0 < infDist x s

Full source

theorem infDist_pos_iff_not_mem_closure (hs : s.Nonempty) :
    x ∉ closure sx ∉ closure s ↔ 0 < infDist x s :=
  (mem_closure_iff_infDist_zero hs).not.trans infDist_nonneg.gt_iff_ne.symm

Positivity of Minimal Distance Characterizes Non-Closure Membership

Informal description

Let $s$ be a nonempty subset of a pseudometric space $\alpha$. For any point $x \in \alpha$, $x$ does not belong to the closure of $s$ if and only if the minimal distance from $x$ to $s$ is strictly positive, i.e., \[ x \notin \overline{s} \leftrightarrow \inf_{y \in s} d(x, y) > 0. \]

IsClosed.mem_iff_infDist_zero theorem

(h : IsClosed s) (hs : s.Nonempty) : x ∈ s ↔ infDist x s = 0

Full source

/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
theorem _root_.IsClosed.mem_iff_infDist_zero (h : IsClosed s) (hs : s.Nonempty) :
    x ∈ sx ∈ s ↔ infDist x s = 0 := by rw [← mem_closure_iff_infDist_zero hs, h.closure_eq]

Characterization of Membership in Closed Sets via Infimum Distance

Informal description

Let $s$ be a nonempty closed subset of a pseudometric space $\alpha$. For any point $x \in \alpha$, we have $x \in s$ if and only if the infimum distance from $x$ to $s$ is zero, i.e., \[ x \in s \leftrightarrow \inf_{y \in s} d(x, y) = 0. \]

IsClosed.not_mem_iff_infDist_pos theorem

(h : IsClosed s) (hs : s.Nonempty) : x ∉ s ↔ 0 < infDist x s

Full source

/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes. -/
theorem _root_.IsClosed.not_mem_iff_infDist_pos (h : IsClosed s) (hs : s.Nonempty) :
    x ∉ sx ∉ s ↔ 0 < infDist x s := by
  simp [h.mem_iff_infDist_zero hs, infDist_nonneg.gt_iff_ne]

Positivity of Minimal Distance Characterizes Non-Membership in Closed Sets

Informal description

Let $s$ be a nonempty closed subset of a pseudometric space $\alpha$. For any point $x \in \alpha$, $x$ does not belong to $s$ if and only if the infimum distance from $x$ to $s$ is strictly positive, i.e., \[ x \notin s \leftrightarrow \inf_{y \in s} d(x, y) > 0. \]

Metric.continuousAt_inv_infDist_pt theorem

(h : x ∉ closure s) : ContinuousAt (fun x ↦ (infDist x s)⁻¹) x

Full source

theorem continuousAt_inv_infDist_pt (h : x ∉ closure s) :
    ContinuousAt (fun x ↦ (infDist x s)⁻¹) x := by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp only [infDist_empty, continuousAt_const]
  · refine (continuous_infDist_pt s).continuousAt.inv₀ ?_
    rwa [Ne, ← mem_closure_iff_infDist_zero hs]

Continuity of Reciprocal Minimal Distance Function Outside Set Closure

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any subset $s \subseteq \alpha$, if $x$ does not belong to the closure of $s$, then the function $x \mapsto (\inf_{y \in s} d(x,y))^{-1}$ is continuous at $x$.

Metric.infDist_image theorem

(hΦ : Isometry Φ) : infDist (Φ x) (Φ '' t) = infDist x t

Full source

/-- The infimum distance is invariant under isometries. -/
theorem infDist_image (hΦ : Isometry Φ) : infDist (Φ x) (Φ '' t) = infDist x t := by
  simp [infDist, infEdist_image hΦ]

Isometry Invariance of Minimal Distance

Informal description

Let $\Phi$ be an isometry between pseudometric spaces. For any point $x$ and subset $t$ in the domain of $\Phi$, the minimal distance from $\Phi(x)$ to the image $\Phi(t)$ equals the minimal distance from $x$ to $t$, i.e., \[ \inf_{y \in t} d(\Phi(x), \Phi(y)) = \inf_{y \in t} d(x, y). \]

Metric.infDist_inter_closedBall_of_mem theorem

(h : y ∈ s) : infDist x (s ∩ closedBall x (dist y x)) = infDist x s

Full source

theorem infDist_inter_closedBall_of_mem (h : y ∈ s) :
    infDist x (s ∩ closedBall x (dist y x)) = infDist x s := by
  replace h : y ∈ s ∩ closedBall x (dist y x) := ⟨h, mem_closedBall.2 le_rfl⟩
  refine le_antisymm ?_ (infDist_le_infDist_of_subset inter_subset_left ⟨y, h⟩)
  refine not_lt.1 fun hlt => ?_
  rcases (infDist_lt_iff ⟨y, h.1⟩).mp hlt with ⟨z, hzs, hz⟩
  rcases le_or_lt (dist z x) (dist y x) with hle | hlt
  · exact hz.not_le (infDist_le_dist_of_mem ⟨hzs, hle⟩)
  · rw [dist_comm z, dist_comm y] at hlt
    exact (hlt.trans hz).not_le (infDist_le_dist_of_mem h)

Minimal Distance to Intersection with Closed Ball Equals Minimal Distance to Set

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any subset $s \subseteq \alpha$, if $y \in s$, then the minimal distance from $x$ to the intersection of $s$ with the closed ball centered at $x$ of radius $\text{dist}(y, x)$ equals the minimal distance from $x$ to $s$. That is, \[ \inf_{z \in s \cap \overline{B}(x, \text{dist}(y, x))} \text{dist}(x, z) = \inf_{z \in s} \text{dist}(x, z). \]

IsCompact.exists_infDist_eq_dist theorem

(h : IsCompact s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, infDist x s = dist x y

Full source

theorem _root_.IsCompact.exists_infDist_eq_dist (h : IsCompact s) (hne : s.Nonempty) (x : α) :
    ∃ y ∈ s, infDist x s = dist x y :=
  let ⟨y, hys, hy⟩ := h.exists_infEdist_eq_edist hne x
  ⟨y, hys, by rw [infDist, dist_edist, hy]⟩

Existence of a Point Attaining Minimal Distance to a Compact Set

Informal description

Let $s$ be a nonempty compact subset of a pseudometric space $\alpha$, and let $x$ be a point in $\alpha$. Then there exists a point $y \in s$ such that the minimal distance from $x$ to $s$ equals the distance from $x$ to $y$, i.e., \[ \inf_{z \in s} \text{dist}(x, z) = \text{dist}(x, y). \]

IsClosed.exists_infDist_eq_dist theorem

[ProperSpace α] (h : IsClosed s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, infDist x s = dist x y

Full source

theorem _root_.IsClosed.exists_infDist_eq_dist [ProperSpace α] (h : IsClosed s) (hne : s.Nonempty)
    (x : α) : ∃ y ∈ s, infDist x s = dist x y := by
  rcases hne with ⟨z, hz⟩
  rw [← infDist_inter_closedBall_of_mem hz]
  set t := s ∩ closedBall x (dist z x)
  have htc : IsCompact t := (isCompact_closedBall x (dist z x)).inter_left h
  have htne : t.Nonempty := ⟨z, hz, mem_closedBall.2 le_rfl⟩
  obtain ⟨y, ⟨hys, -⟩, hyd⟩ : ∃ y ∈ t, infDist x t = dist x y := htc.exists_infDist_eq_dist htne x
  exact ⟨y, hys, hyd⟩

Existence of Minimal Distance Attaining Point for Closed Sets in Proper Metric Spaces

Informal description

Let $\alpha$ be a proper metric space, $s$ a nonempty closed subset of $\alpha$, and $x$ a point in $\alpha$. Then there exists a point $y \in s$ such that the minimal distance from $x$ to $s$ equals the distance from $x$ to $y$, i.e., \[ \inf_{z \in s} \text{dist}(x, z) = \text{dist}(x, y). \]

Metric.exists_mem_closure_infDist_eq_dist theorem

[ProperSpace α] (hne : s.Nonempty) (x : α) : ∃ y ∈ closure s, infDist x s = dist x y

Full source

theorem exists_mem_closure_infDist_eq_dist [ProperSpace α] (hne : s.Nonempty) (x : α) :
    ∃ y ∈ closure s, infDist x s = dist x y := by
  simpa only [infDist_closure] using isClosed_closure.exists_infDist_eq_dist hne.closure x

Existence of Minimal Distance Attaining Point in Closure for Nonempty Sets in Proper Metric Spaces

Informal description

Let $\alpha$ be a proper metric space, $s$ a nonempty subset of $\alpha$, and $x$ a point in $\alpha$. Then there exists a point $y$ in the closure of $s$ such that the minimal distance from $x$ to $s$ equals the distance from $x$ to $y$, i.e., \[ \inf_{z \in s} d(x, z) = d(x, y). \]

Metric.infNndist definition

(x : α) (s : Set α) : ℝ≥0

Full source

/-- The minimal distance of a point to a set as a `ℝ≥0` -/
def infNndist (x : α) (s : Set α) : ℝ≥0 :=
  ENNReal.toNNReal (infEdist x s)

Minimal nonnegative distance from a point to a set

Informal description

Given a point $ x $ in a pseudometric space $ \alpha $ and a subset $ s \subseteq \alpha $, the minimal nonnegative distance from $ x $ to $ s $ is defined as the nonnegative real number obtained by converting the infimum of the extended distances from $ x $ to all points in $ s $. If the infimum is infinite, it returns $ 0 $.

Metric.coe_infNndist theorem

: (infNndist x s : ℝ) = infDist x s

Full source

@[simp]
theorem coe_infNndist : (infNndist x s : ℝ) = infDist x s :=
  rfl

Coercion of Minimal Nonnegative Distance to Minimal Distance

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any subset $s \subseteq \alpha$, the real number obtained by coercing the minimal nonnegative distance $\text{infNndist}(x, s)$ is equal to the minimal distance $\text{infDist}(x, s)$.

Metric.lipschitz_infNndist_pt theorem

(s : Set α) : LipschitzWith 1 fun x => infNndist x s

Full source

/-- The minimal distance to a set (as `ℝ≥0`) is Lipschitz in point with constant 1 -/
theorem lipschitz_infNndist_pt (s : Set α) : LipschitzWith 1 fun x => infNndist x s :=
  LipschitzWith.of_le_add fun _ _ => infDist_le_infDist_add_dist

Lipschitz continuity of minimal distance function with constant 1

Informal description

For any subset $s$ of a pseudometric space $\alpha$, the function $x \mapsto \inf_{y \in s} d(x, y)$ (where the infimum is taken as a nonnegative real number) is Lipschitz continuous with constant 1. That is, for any two points $x_1, x_2 \in \alpha$, \[ |\inf_{y \in s} d(x_1, y) - \inf_{y \in s} d(x_2, y)| \leq d(x_1, x_2). \]

Metric.uniformContinuous_infNndist_pt theorem

(s : Set α) : UniformContinuous fun x => infNndist x s

Full source

/-- The minimal distance to a set (as `ℝ≥0`) is uniformly continuous in point -/
theorem uniformContinuous_infNndist_pt (s : Set α) : UniformContinuous fun x => infNndist x s :=
  (lipschitz_infNndist_pt s).uniformContinuous

Uniform continuity of minimal distance function to a set

Informal description

For any subset $s$ of a pseudometric space $\alpha$, the function $x \mapsto \inf_{y \in s} d(x, y)$ (where the infimum is taken as a nonnegative real number) is uniformly continuous. That is, for any $\epsilon > 0$, there exists $\delta > 0$ such that for all $x_1, x_2 \in \alpha$ with $d(x_1, x_2) < \delta$, we have \[ |\inf_{y \in s} d(x_1, y) - \inf_{y \in s} d(x_2, y)| < \epsilon. \]

Metric.continuous_infNndist_pt theorem

(s : Set α) : Continuous fun x => infNndist x s

Full source

/-- The minimal distance to a set (as `ℝ≥0`) is continuous in point -/
theorem continuous_infNndist_pt (s : Set α) : Continuous fun x => infNndist x s :=
  (uniformContinuous_infNndist_pt s).continuous

Continuity of the Minimal Distance Function to a Set

Informal description

For any subset $s$ of a pseudometric space $\alpha$, the function $x \mapsto \inf_{y \in s} d(x, y)$ (where the infimum is taken as a nonnegative real number) is continuous. That is, for any point $x_0 \in \alpha$ and any $\epsilon > 0$, there exists $\delta > 0$ such that for all $x \in \alpha$ with $d(x, x_0) < \delta$, we have \[ |\inf_{y \in s} d(x, y) - \inf_{y \in s} d(x_0, y)| < \epsilon. \]

Metric.hausdorffDist definition

(s t : Set α) : ℝ

Full source

/-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
be `0`, arbitrarily. -/
def hausdorffDist (s t : Set α) : ℝ :=
  ENNReal.toReal (hausdorffEdist s t)

Hausdorff distance between sets in a metric space

Informal description

The Hausdorff distance between two subsets $ s $ and $ t $ of a metric space $ \alpha $ is the smallest nonnegative real number $ d $ such that every point in $ s $ is within distance $ d $ of some point in $ t $, and vice versa. If no such $ d $ exists (i.e., if the Hausdorff extended distance is infinite), the distance is defined to be 0. Formally, it is given by the real-valued conversion of the Hausdorff extended distance: \[ \text{hausdorffDist}(s, t) = \text{toReal}(\text{hausdorffEdist}(s, t)) \] where $\text{hausdorffEdist}(s, t)$ is the extended distance defined in terms of the infimum distances between points of $ s $ and $ t $.

Metric.hausdorffDist_nonneg theorem

: 0 ≤ hausdorffDist s t

Full source

/-- The Hausdorff distance is nonnegative. -/
theorem hausdorffDist_nonneg : 0 ≤ hausdorffDist s t := by simp [hausdorffDist]

Nonnegativity of Hausdorff Distance

Informal description

For any two subsets $s$ and $t$ of a pseudometric space, the Hausdorff distance between them is nonnegative, i.e., $\text{hausdorffDist}(s, t) \geq 0$.

Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded theorem

(hs : s.Nonempty) (ht : t.Nonempty) (bs : IsBounded s) (bt : IsBounded t) : hausdorffEdist s t ≠ ⊤

Full source

/-- If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff
edistance. -/
theorem hausdorffEdist_ne_top_of_nonempty_of_bounded (hs : s.Nonempty) (ht : t.Nonempty)
    (bs : IsBounded s) (bt : IsBounded t) : hausdorffEdisthausdorffEdist s t ≠ ⊤ := by
  rcases hs with ⟨cs, hcs⟩
  rcases ht with ⟨ct, hct⟩
  rcases bs.subset_closedBall ct with ⟨rs, hrs⟩
  rcases bt.subset_closedBall cs with ⟨rt, hrt⟩
  have : hausdorffEdist s t ≤ ENNReal.ofReal (max rs rt) := by
    apply hausdorffEdist_le_of_mem_edist
    · intro x xs
      exists ct, hct
      have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this
    · intro x xt
      exists cs, hcs
      have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this
  exact ne_top_of_le_ne_top ENNReal.ofReal_ne_top this

Finite Hausdorff Distance for Nonempty Bounded Sets

Informal description

For any nonempty and bounded subsets $s$ and $t$ of a pseudometric space $\alpha$, the Hausdorff extended distance between $s$ and $t$ is finite, i.e., $\text{hausdorffEdist}(s, t) \neq \infty$.

Metric.hausdorffDist_self_zero theorem

: hausdorffDist s s = 0

Full source

/-- The Hausdorff distance between a set and itself is zero. -/
@[simp]
theorem hausdorffDist_self_zero : hausdorffDist s s = 0 := by simp [hausdorffDist]

Hausdorff Distance of a Set to Itself Vanishes

Informal description

For any subset $s$ of a metric space, the Hausdorff distance between $s$ and itself is zero, i.e., $\text{hausdorffDist}(s, s) = 0$.

Metric.hausdorffDist_comm theorem

: hausdorffDist s t = hausdorffDist t s

Full source

/-- The Hausdorff distances from `s` to `t` and from `t` to `s` coincide. -/
theorem hausdorffDist_comm : hausdorffDist s t = hausdorffDist t s := by
  simp [hausdorffDist, hausdorffEdist_comm]

Symmetry of Hausdorff Distance: $d_H(s, t) = d_H(t, s)$

Informal description

For any two subsets $s$ and $t$ of a metric space, the Hausdorff distance from $s$ to $t$ equals the Hausdorff distance from $t$ to $s$, i.e., \[ d_H(s, t) = d_H(t, s). \]

Metric.hausdorffDist_empty theorem

: hausdorffDist s ∅ = 0

Full source

/-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value `∞` instead, use `EMetric.hausdorffEdist`, which takes values in `ℝ≥0∞`). -/
@[simp]
theorem hausdorffDist_empty : hausdorffDist s ∅ = 0 := by
  rcases s.eq_empty_or_nonempty with h | h
  · simp [h]
  · simp [hausdorffDist, hausdorffEdist_empty h]

Hausdorff Distance to Empty Set Vanishes

Informal description

For any subset $s$ of a metric space, the Hausdorff distance between $s$ and the empty set is zero, i.e., $\text{hausdorffDist}(s, \emptyset) = 0$.

Metric.hausdorffDist_empty' theorem

: hausdorffDist ∅ s = 0

Full source

/-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
value `∞` instead, use `EMetric.hausdorffEdist`, which takes values in `ℝ≥0∞`). -/
@[simp]
theorem hausdorffDist_empty' : hausdorffDist ∅ s = 0 := by simp [hausdorffDist_comm]

Hausdorff Distance from Empty Set Vanishes

Informal description

For any subset $s$ of a metric space, the Hausdorff distance between the empty set and $s$ is zero, i.e., $\text{hausdorffDist}(\emptyset, s) = 0$.

Metric.hausdorffDist_le_of_infDist theorem

 {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, infDist x t ≤ r) (H2 : ∀ x ∈ t, infDist x s ≤ r) : hausdorffDist s t ≤ r

Full source

/-- Bounding the Hausdorff distance by bounding the distance of any point
in each set to the other set -/
theorem hausdorffDist_le_of_infDist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, infDist x t ≤ r)
    (H2 : ∀ x ∈ t, infDist x s ≤ r) : hausdorffDist s t ≤ r := by
  rcases s.eq_empty_or_nonempty with hs | hs
  · rwa [hs, hausdorffDist_empty']
  rcases t.eq_empty_or_nonempty with ht | ht
  · rwa [ht, hausdorffDist_empty]
  have : hausdorffEdist s t ≤ ENNReal.ofReal r := by
    apply hausdorffEdist_le_of_infEdist _ _
    · simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top ht) hr] using H1
    · simpa only [infDist, ← ENNReal.le_ofReal_iff_toReal_le (infEdist_ne_top hs) hr] using H2
  exact ENNReal.toReal_le_of_le_ofReal hr this

Upper Bound on Hausdorff Distance via Pointwise Minimal Distances

Informal description

For any nonnegative real number $r \geq 0$ and any two subsets $s$ and $t$ in a metric space, if for every point $x \in s$ the minimal distance from $x$ to $t$ is at most $r$, and similarly for every point $x \in t$ the minimal distance from $x$ to $s$ is at most $r$, then the Hausdorff distance between $s$ and $t$ is at most $r$.

Metric.hausdorffDist_le_of_mem_dist theorem

 {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r) (H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) :
  hausdorffDist s t ≤ r

Full source

/-- Bounding the Hausdorff distance by exhibiting, for any point in each set,
another point in the other set at controlled distance -/
theorem hausdorffDist_le_of_mem_dist {r : ℝ} (hr : 0 ≤ r) (H1 : ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ r)
    (H2 : ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ r) : hausdorffDist s t ≤ r := by
  apply hausdorffDist_le_of_infDist hr
  · intro x xs
    rcases H1 x xs with ⟨y, yt, hy⟩
    exact le_trans (infDist_le_dist_of_mem yt) hy
  · intro x xt
    rcases H2 x xt with ⟨y, ys, hy⟩
    exact le_trans (infDist_le_dist_of_mem ys) hy

Hausdorff Distance Bounded by Pointwise Distance Conditions

Informal description

For any nonnegative real number $r \geq 0$ and any two subsets $s$ and $t$ in a metric space, if for every point $x \in s$ there exists a point $y \in t$ such that the distance between $x$ and $y$ is at most $r$, and similarly for every point $x \in t$ there exists a point $y \in s$ such that the distance between $x$ and $y$ is at most $r$, then the Hausdorff distance between $s$ and $t$ is at most $r$.

Metric.hausdorffDist_le_diam theorem

(hs : s.Nonempty) (bs : IsBounded s) (ht : t.Nonempty) (bt : IsBounded t) : hausdorffDist s t ≤ diam (s ∪ t)

Full source

/-- The Hausdorff distance is controlled by the diameter of the union. -/
theorem hausdorffDist_le_diam (hs : s.Nonempty) (bs : IsBounded s) (ht : t.Nonempty)
    (bt : IsBounded t) : hausdorffDist s t ≤ diam (s ∪ t) := by
  rcases hs with ⟨x, xs⟩
  rcases ht with ⟨y, yt⟩
  refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_
  · exact fun z hz => ⟨y, yt, dist_le_diam_of_mem (bs.union bt) (subset_union_left hz)
      (subset_union_right yt)⟩
  · exact fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz)
      (subset_union_left xs)⟩

Hausdorff distance bounded by diameter of union

Informal description

For any nonempty bounded subsets $s$ and $t$ of a metric space, the Hausdorff distance between $s$ and $t$ is bounded above by the diameter of their union, i.e., \[ d_H(s, t) \leq \text{diam}(s \cup t). \]

Metric.infDist_le_hausdorffDist_of_mem theorem

(hx : x ∈ s) (fin : hausdorffEdist s t ≠ ⊤) : infDist x t ≤ hausdorffDist s t

Full source

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

Minimal Distance to Set Bounded by Hausdorff Distance

Informal description

For any point $x$ in a subset $s$ of a metric space, if the Hausdorff extended distance between $s$ and another subset $t$ is finite, then the minimal distance from $x$ to $t$ is bounded above by the Hausdorff distance between $s$ and $t$, i.e., \[ \inf_{y \in t} d(x, y) \leq \text{hausdorffDist}(s, t). \]

Metric.exists_dist_lt_of_hausdorffDist_lt theorem

{r : ℝ} (h : x ∈ s) (H : hausdorffDist s t < r) (fin : hausdorffEdist s t ≠ ⊤) : ∃ y ∈ t, dist x y < r

Full source

/-- 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 : x ∈ s) (H : hausdorffDist s t < r)
    (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) : ∃ y ∈ t, dist x y < r := by
  have r0 : 0 < r := lt_of_le_of_lt hausdorffDist_nonneg H
  have : hausdorffEdist s t < ENNReal.ofReal r := by
    rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H
  rcases exists_edist_lt_of_hausdorffEdist_lt h this with ⟨y, hy, yr⟩
  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff r0] at yr
  exact ⟨y, hy, yr⟩

Existence of Close Points under Hausdorff Distance Condition in Metric Spaces

Informal description

For any point $x$ in a subset $s$ of a metric space, if the Hausdorff distance between $s$ and another subset $t$ is less than a real number $r$ and the extended Hausdorff distance is finite, then there exists a point $y \in t$ such that the distance between $x$ and $y$ is less than $r$, i.e., \[ \text{hausdorffDist}(s, t) < r \implies \exists y \in t, d(x, y) < r. \]

Metric.exists_dist_lt_of_hausdorffDist_lt' theorem

{r : ℝ} (h : y ∈ t) (H : hausdorffDist s t < r) (fin : hausdorffEdist s t ≠ ⊤) : ∃ x ∈ s, dist x y < r

Full source

/-- 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 : hausdorffEdisthausdorffEdist 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

Existence of Close Points in First Set under Hausdorff Distance Condition

Informal description

For any point $y$ in a subset $t$ of a metric space, if the Hausdorff distance between subsets $s$ and $t$ is less than a real number $r$ and the extended Hausdorff distance is finite, then there exists a point $x \in s$ such that the distance between $x$ and $y$ is less than $r$, i.e., \[ d_H(s, t) < r \implies \exists x \in s, d(x, y) < r. \]

Metric.infDist_le_infDist_add_hausdorffDist theorem

(fin : hausdorffEdist s t ≠ ⊤) : infDist x t ≤ infDist x s + hausdorffDist s t

Full source

/-- The infimum distance to `s` and `t` are the same, up to the Hausdorff distance
between `s` and `t` -/
theorem infDist_le_infDist_add_hausdorffDist (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) :
    infDist x t ≤ infDist x s + hausdorffDist s t := by
  refine toReal_le_add' infEdist_le_infEdist_add_hausdorffEdist (fun h ↦ ?_) (flip absurd fin)
  rw [infEdist_eq_top_iff, ← not_nonempty_iff_eq_empty] at h ⊢
  rw [hausdorffEdist_comm] at fin
  exact mt (nonempty_of_hausdorffEdist_ne_top · fin) h

Triangle Inequality for Minimal Distance and Hausdorff Distance in Metric Spaces

Informal description

Let $s$ and $t$ be subsets of a metric space $\alpha$, and let $x \in \alpha$. If the Hausdorff extended distance between $s$ and $t$ is finite, then the minimal distance from $x$ to $t$ is bounded above by the sum of the minimal distance from $x$ to $s$ and the Hausdorff distance between $s$ and $t$, i.e., \[ \inf_{y \in t} d(x, y) \leq \inf_{z \in s} d(x, z) + \text{hausdorffDist}(s, t). \]

Metric.hausdorffDist_image theorem

(h : Isometry Φ) : hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t

Full source

/-- The Hausdorff distance is invariant under isometries. -/
theorem hausdorffDist_image (h : Isometry Φ) :
    hausdorffDist (Φ '' s) (Φ '' t) = hausdorffDist s t := by
  simp [hausdorffDist, hausdorffEdist_image h]

Isometry Invariance of Hausdorff Distance

Informal description

Let $\Phi$ be an isometry between pseudometric spaces. For any two subsets $s$ and $t$ in the domain of $\Phi$, the Hausdorff distance between the images $\Phi(s)$ and $\Phi(t)$ equals the Hausdorff distance between $s$ and $t$, i.e., \[ \text{hausdorffDist}(\Phi(s), \Phi(t)) = \text{hausdorffDist}(s, t). \]

Metric.hausdorffDist_triangle theorem

(fin : hausdorffEdist s t ≠ ⊤) : hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Full source

/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffDist_triangle (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) :
    hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u := by
  refine toReal_le_add' hausdorffEdist_triangle (flip absurd fin) (not_imp_not.1 fun h ↦ ?_)
  rw [hausdorffEdist_comm] at fin
  exact ne_top_of_le_ne_top (add_ne_top.2 ⟨fin, h⟩) hausdorffEdist_triangle

Triangle Inequality for Hausdorff Distance in Metric Spaces

Informal description

For any subsets $s$, $t$, and $u$ of a metric space, if the Hausdorff extended distance between $s$ and $t$ is finite, then the Hausdorff distance satisfies the triangle inequality: \[ \text{hausdorffDist}(s, u) \leq \text{hausdorffDist}(s, t) + \text{hausdorffDist}(t, u). \]

Metric.hausdorffDist_triangle' theorem

(fin : hausdorffEdist t u ≠ ⊤) : hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Full source

/-- The Hausdorff distance satisfies the triangle inequality. -/
theorem hausdorffDist_triangle' (fin : hausdorffEdisthausdorffEdist t u ≠ ⊤) :
    hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u := by
  rw [hausdorffEdist_comm] at fin
  have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
    hausdorffDist_triangle fin
  simpa [add_comm, hausdorffDist_comm] using I

Triangle Inequality for Hausdorff Distance: $d_H(s, u) \leq d_H(s, t) + d_H(t, u)$ when $d_H(t, u) < \infty$

Informal description

For any subsets $s$, $t$, and $u$ of a metric space, if the Hausdorff extended distance between $t$ and $u$ is finite, then the Hausdorff distance satisfies the triangle inequality: \[ d_H(s, u) \leq d_H(s, t) + d_H(t, u). \]

Metric.hausdorffDist_self_closure theorem

: hausdorffDist s (closure s) = 0

Full source

/-- The Hausdorff distance between a set and its closure vanishes. -/
@[simp]
theorem hausdorffDist_self_closure : hausdorffDist s (closure s) = 0 := by simp [hausdorffDist]

Hausdorff Distance Between Set and Its Closure Vanishes

Informal description

For any subset $s$ of a metric space, the Hausdorff distance between $s$ and its closure $\overline{s}$ is zero, i.e., \[ \text{hausdorffDist}(s, \overline{s}) = 0. \]

Metric.hausdorffDist_closure₁ theorem

: hausdorffDist (closure s) t = hausdorffDist s t

Full source

/-- Replacing a set by its closure does not change the Hausdorff distance. -/
@[simp]
theorem hausdorffDist_closure₁ : hausdorffDist (closure s) t = hausdorffDist s t := by
  simp [hausdorffDist]

Hausdorff Distance Invariance Under Closure of First Set

Informal description

For any subsets $s$ and $t$ of a metric space, the Hausdorff distance between the closure of $s$ and $t$ is equal to the Hausdorff distance between $s$ and $t$, i.e., \[ \text{hausdorffDist}(\overline{s}, t) = \text{hausdorffDist}(s, t). \]

Metric.hausdorffDist_closure₂ theorem

: hausdorffDist s (closure t) = hausdorffDist s t

Full source

/-- Replacing a set by its closure does not change the Hausdorff distance. -/
@[simp]
theorem hausdorffDist_closure₂ : hausdorffDist s (closure t) = hausdorffDist s t := by
  simp [hausdorffDist]

Hausdorff Distance Invariance Under Closure of Second Set

Informal description

For any subsets $s$ and $t$ of a metric space, the Hausdorff distance between $s$ and the closure of $t$ is equal to the Hausdorff distance between $s$ and $t$, i.e., \[ d_H(s, \overline{t}) = d_H(s, t). \]

Metric.hausdorffDist_closure theorem

: hausdorffDist (closure s) (closure t) = hausdorffDist s t

Full source

/-- The Hausdorff distances between two sets and their closures coincide. -/
theorem hausdorffDist_closure : hausdorffDist (closure s) (closure t) = hausdorffDist s t := by
  simp [hausdorffDist]

Hausdorff Distance Invariance Under Closure

Informal description

For any subsets $s$ and $t$ of a metric space, the Hausdorff distance between their closures equals the Hausdorff distance between the original sets, i.e., \[ \text{hausdorffDist}(\overline{s}, \overline{t}) = \text{hausdorffDist}(s, t). \]

Metric.hausdorffDist_zero_iff_closure_eq_closure theorem

(fin : hausdorffEdist s t ≠ ⊤) : hausdorffDist s t = 0 ↔ closure s = closure t

Full source

/-- Two sets are at zero Hausdorff distance if and only if they have the same closures. -/
theorem hausdorffDist_zero_iff_closure_eq_closure (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) :
    hausdorffDisthausdorffDist s t = 0 ↔ closure s = closure t := by
  simp [← hausdorffEdist_zero_iff_closure_eq_closure, hausdorffDist,
    ENNReal.toReal_eq_zero_iff, fin]

Hausdorff Distance Zero Characterizes Equal Closures in Pseudometric Spaces

Informal description

Let $s$ and $t$ be subsets of a pseudometric space $\alpha$, and assume the Hausdorff extended distance between them is finite. Then the Hausdorff distance between $s$ and $t$ is zero if and only if their closures are equal, i.e., \[ \text{hausdorffDist}(s, t) = 0 \leftrightarrow \text{closure}(s) = \text{closure}(t). \]

IsClosed.hausdorffDist_zero_iff_eq theorem

(hs : IsClosed s) (ht : IsClosed t) (fin : hausdorffEdist s t ≠ ⊤) : hausdorffDist s t = 0 ↔ s = t

Full source

/-- Two closed sets are at zero Hausdorff distance if and only if they coincide. -/
theorem _root_.IsClosed.hausdorffDist_zero_iff_eq (hs : IsClosed s) (ht : IsClosed t)
    (fin : hausdorffEdisthausdorffEdist s t ≠ ⊤) : hausdorffDisthausdorffDist s t = 0 ↔ s = t := by
  simp [← hausdorffEdist_zero_iff_eq_of_closed hs ht, hausdorffDist, ENNReal.toReal_eq_zero_iff,
    fin]

Hausdorff Distance Zero Characterizes Equality for Closed Sets in Metric Spaces

Informal description

For any two closed subsets $s$ and $t$ in a metric space $\alpha$, if the Hausdorff extended distance between them is finite, then the Hausdorff distance $\text{hausdorffDist}(s, t) = 0$ if and only if $s = t$.

Mathlib.Topology.MetricSpace.HausdorffDistance

Main definitions

Main results

Tags