mathlib docs: topology.metric_space.hausdorff

source

def emetric.inf_edist {α : Type u} [emetric_space α] :

α → set α → ennreal

The minimal edistance of a point to a set

Equations

emetric.inf_edist x s = has_Inf.Inf (has_edist.edist x '' s)

source

@[simp]

theorem emetric.inf_edist_empty {α : Type u} [emetric_space α] {x : α} :

emetric.inf_edist x ∅ = ⊤

source

@[simp]

theorem emetric.inf_edist_union {α : Type u} [emetric_space α] {x : α} {s t : set α} :

emetric.inf_edist x (s ∪ t) = emetric.inf_edist x s ⊓ emetric.inf_edist x t

The edist to a union is the minimum of the edists

source

@[simp]

theorem emetric.inf_edist_singleton {α : Type u} [emetric_space α] {x y : α} :

emetric.inf_edist x {y} = has_edist.edist x y

The edist to a singleton is the edistance to the single point of this singleton

source

theorem emetric.inf_edist_le_edist_of_mem {α : Type u} [emetric_space α] {x y : α} {s : set α} :

y ∈ s → emetric.inf_edist x s ≤ has_edist.edist x y

The edist to a set is bounded above by the edist to any of its points

source

theorem emetric.inf_edist_zero_of_mem {α : Type u} [emetric_space α] {x : α} {s : set α} :

x ∈ s → emetric.inf_edist x s = 0

If a point x belongs to s, then its edist to s vanishes

source

theorem emetric.inf_edist_le_inf_edist_of_subset {α : Type u} [emetric_space α] {x : α} {s t : set α} :

s ⊆ t → emetric.inf_edist x t ≤ emetric.inf_edist x s

The edist is monotonous with respect to inclusion

source

theorem emetric.exists_edist_lt_of_inf_edist_lt {α : Type u} [emetric_space α] {x : α} {s : set α} {r : ennreal} :

emetric.inf_edist x s < r → (∃ (y : α) (H : y ∈ s), has_edist.edist x y < r)

If the edist to a set is < r, there exists a point in the set at edistance < r

source

theorem emetric.inf_edist_le_inf_edist_add_edist {α : Type u} [emetric_space α] {x y : α} {s : set α} :

emetric.inf_edist x s ≤ emetric.inf_edist y s + has_edist.edist x y

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

source

theorem emetric.continuous_inf_edist {α : Type u} [emetric_space α] {s : set α} :

continuous (λ (x : α), emetric.inf_edist x s)

The edist to a set depends continuously on the point

source

theorem emetric.inf_edist_closure {α : Type u} [emetric_space α] {x : α} {s : set α} :

emetric.inf_edist x (closure s) = emetric.inf_edist x s

The edist to a set and to its closure coincide

source

theorem emetric.mem_closure_iff_inf_edist_zero {α : Type u} [emetric_space α] {x : α} {s : set α} :

x ∈ closure s ↔ emetric.inf_edist x s = 0

A point belongs to the closure of s iff its infimum edistance to this set vanishes

source

theorem emetric.mem_iff_ind_edist_zero_of_closed {α : Type u} [emetric_space α] {x : α} {s : set α} :

is_closed s → (x ∈ s ↔ emetric.inf_edist x s = 0)

Given a closed set s, a point belongs to s iff its infimum edistance to this set vanishes

source

theorem emetric.inf_edist_image {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {x : α} {t : set α} {Φ : α → β} :

isometry Φ → emetric.inf_edist (Φ x) (Φ '' t) = emetric.inf_edist x t

The infimum edistance is invariant under isometries

source

def emetric.Hausdorff_edist {α : Type u} [emetric_space α] :

set α → set α → ennreal

The Hausdorff edistance between two sets is the smallest r such that each set is contained in the r-neighborhood of the other one

Equations

emetric.Hausdorff_edist s t = has_Sup.Sup ((λ (x : α), emetric.inf_edist x t) '' s) ⊔ has_Sup.Sup ((λ (x : α), emetric.inf_edist x s) '' t)

source

theorem emetric.Hausdorff_edist_def {α : Type u} [emetric_space α] (s t : set α) :

emetric.Hausdorff_edist s t = has_Sup.Sup ((λ (x : α), emetric.inf_edist x t) '' s) ⊔ has_Sup.Sup ((λ (x : α), emetric.inf_edist x s) '' t)

source

@[simp]

theorem emetric.Hausdorff_edist_self {α : Type u} [emetric_space α] {s : set α} :

emetric.Hausdorff_edist s s = 0

The Hausdorff edistance of a set to itself vanishes

source

theorem emetric.Hausdorff_edist_comm {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist s t = emetric.Hausdorff_edist t s

The Haudorff edistances of s to t and of t to s coincide

source

theorem emetric.Hausdorff_edist_le_of_inf_edist {α : Type u} [emetric_space α] {s t : set α} {r : ennreal} :

(∀ (x : α), x ∈ s → emetric.inf_edist x t ≤ r) → (∀ (x : α), x ∈ t → emetric.inf_edist x s ≤ r) → emetric.Hausdorff_edist s t ≤ r

Bounding the Hausdorff edistance by bounding the edistance of any point in each set to the other set

source

theorem emetric.Hausdorff_edist_le_of_mem_edist {α : Type u} [emetric_space α] {s t : set α} {r : ennreal} :

(∀ (x : α), x ∈ s → (∃ (y : α) (H : y ∈ t), has_edist.edist x y ≤ r)) → (∀ (x : α), x ∈ t → (∃ (y : α) (H : y ∈ s), has_edist.edist x y ≤ r)) → emetric.Hausdorff_edist s t ≤ r

Bounding the Hausdorff edistance by exhibiting, for any point in each set, another point in the other set at controlled distance

source

theorem emetric.inf_edist_le_Hausdorff_edist_of_mem {α : Type u} [emetric_space α] {x : α} {s t : set α} :

x ∈ s → emetric.inf_edist x t ≤ emetric.Hausdorff_edist s t

The distance to a set is controlled by the Hausdorff distance

source

theorem emetric.exists_edist_lt_of_Hausdorff_edist_lt {α : Type u} [emetric_space α] {x : α} {s t : set α} {r : ennreal} :

x ∈ s → emetric.Hausdorff_edist s t < r → (∃ (y : α) (H : y ∈ t), has_edist.edist x y < r)

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

source

theorem emetric.inf_edist_le_inf_edist_add_Hausdorff_edist {α : Type u} [emetric_space α] {x : α} {s t : set α} :

emetric.inf_edist x t ≤ emetric.inf_edist x s + emetric.Hausdorff_edist s t

The distance from x to s or t is controlled in terms of the Hausdorff distance between s and t

source

theorem emetric.Hausdorff_edist_image {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {s t : set α} {Φ : α → β} :

isometry Φ → emetric.Hausdorff_edist (Φ '' s) (Φ '' t) = emetric.Hausdorff_edist s t

The Hausdorff edistance is invariant under eisometries

source

theorem emetric.Hausdorff_edist_le_ediam {α : Type u} [emetric_space α] {s t : set α} :

s.nonempty → t.nonempty → emetric.Hausdorff_edist s t ≤ emetric.diam (s ∪ t)

The Hausdorff distance is controlled by the diameter of the union

source

theorem emetric.Hausdorff_edist_triangle {α : Type u} [emetric_space α] {s t u : set α} :

emetric.Hausdorff_edist s u ≤ emetric.Hausdorff_edist s t + emetric.Hausdorff_edist t u

The Hausdorff distance satisfies the triangular inequality

source

@[simp]

theorem emetric.Hausdorff_edist_self_closure {α : Type u} [emetric_space α] {s : set α} :

emetric.Hausdorff_edist s (closure s) = 0

The Hausdorff edistance between a set and its closure vanishes

source

@[simp]

theorem emetric.Hausdorff_edist_closure₁ {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist (closure s) t = emetric.Hausdorff_edist s t

Replacing a set by its closure does not change the Hausdorff edistance.

source

@[simp]

theorem emetric.Hausdorff_edist_closure₂ {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist s (closure t) = emetric.Hausdorff_edist s t

Replacing a set by its closure does not change the Hausdorff edistance.

source

@[simp]

theorem emetric.Hausdorff_edist_closure {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist (closure s) (closure t) = emetric.Hausdorff_edist s t

The Hausdorff edistance between sets or their closures is the same

source

theorem emetric.Hausdorff_edist_zero_iff_closure_eq_closure {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist s t = 0 ↔ closure s = closure t

Two sets are at zero Hausdorff edistance if and only if they have the same closure

source

theorem emetric.Hausdorff_edist_zero_iff_eq_of_closed {α : Type u} [emetric_space α] {s t : set α} :

is_closed s → is_closed t → (emetric.Hausdorff_edist s t = 0 ↔ s = t)

Two closed sets are at zero Hausdorff edistance if and only if they coincide

source

theorem emetric.Hausdorff_edist_empty {α : Type u} [emetric_space α] {s : set α} :

s.nonempty → emetric.Hausdorff_edist s ∅ = ⊤

The Haudorff edistance to the empty set is infinite

source

theorem emetric.nonempty_of_Hausdorff_edist_ne_top {α : Type u} [emetric_space α] {s t : set α} :

s.nonempty → emetric.Hausdorff_edist s t ≠ ⊤ → t.nonempty

If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty

source

theorem emetric.empty_or_nonempty_of_Hausdorff_edist_ne_top {α : Type u} [emetric_space α] {s t : set α} :

emetric.Hausdorff_edist s t ≠ ⊤ → s = ∅ ∧ t = ∅ ∨ s.nonempty ∧ t.nonempty

source

def metric.inf_dist {α : Type u} [metric_space α] :

α → set α → ℝ

The minimal distance of a point to a set

Equations

metric.inf_dist x s = (emetric.inf_edist x s).to_real

source

theorem metric.inf_dist_nonneg {α : Type u} [metric_space α] {s : set α} {x : α} :

0 ≤ metric.inf_dist x s

the minimal distance is always nonnegative

source

@[simp]

theorem metric.inf_dist_empty {α : Type u} [metric_space α] {x : α} :

metric.inf_dist x ∅ = 0

the minimal distance to the empty set is 0 (if you want to have the more reasonable value ∞ instead, use inf_edist, which takes values in ennreal)

source

theorem metric.inf_edist_ne_top {α : Type u} [metric_space α] {s : set α} {x : α} :

s.nonempty → emetric.inf_edist x s ≠ ⊤

In a metric space, the minimal edistance to a nonempty set is finite

source

theorem metric.inf_dist_zero_of_mem {α : Type u} [metric_space α] {s : set α} {x : α} :

x ∈ s → metric.inf_dist x s = 0

The minimal distance of a point to a set containing it vanishes

source

@[simp]

theorem metric.inf_dist_singleton {α : Type u} [metric_space α] {x y : α} :

metric.inf_dist x {y} = has_dist.dist x y

The minimal distance to a singleton is the distance to the unique point in this singleton

source

theorem metric.inf_dist_le_dist_of_mem {α : Type u} [metric_space α] {s : set α} {x y : α} :

y ∈ s → metric.inf_dist x s ≤ has_dist.dist x y

The minimal distance to a set is bounded by the distance to any point in this set

source

theorem metric.inf_dist_le_inf_dist_of_subset {α : Type u} [metric_space α] {s t : set α} {x : α} :

s ⊆ t → s.nonempty → metric.inf_dist x t ≤ metric.inf_dist x s

The minimal distance is monotonous with respect to inclusion

source

theorem metric.exists_dist_lt_of_inf_dist_lt {α : Type u} [metric_space α] {s : set α} {x : α} {r : ℝ} :

metric.inf_dist x s < r → s.nonempty → (∃ (y : α) (H : y ∈ s), has_dist.dist x y < r)

If the minimal distance to a set is <r, there exists a point in this set at distance <r

source

theorem metric.inf_dist_le_inf_dist_add_dist {α : Type u} [metric_space α] {s : set α} {x y : α} :

metric.inf_dist x s ≤ metric.inf_dist y s + has_dist.dist x y

The minimal distance from x to s is bounded by the distance from y to s, modulo the distance between x and y

source

theorem metric.lipschitz_inf_dist_pt {α : Type u} [metric_space α] (s : set α) :

lipschitz_with 1 (λ (x : α), metric.inf_dist x s)

The minimal distance to a set is Lipschitz in point with constant 1

source

theorem metric.uniform_continuous_inf_dist_pt {α : Type u} [metric_space α] (s : set α) :

uniform_continuous (λ (x : α), metric.inf_dist x s)

The minimal distance to a set is uniformly continuous in point

source

theorem metric.continuous_inf_dist_pt {α : Type u} [metric_space α] (s : set α) :

continuous (λ (x : α), metric.inf_dist x s)

The minimal distance to a set is continuous in point

source

theorem metric.inf_dist_eq_closure {α : Type u} [metric_space α] {s : set α} {x : α} :

metric.inf_dist x (closure s) = metric.inf_dist x s

The minimal distance to a set and its closure coincide

source

theorem metric.mem_closure_iff_inf_dist_zero {α : Type u} [metric_space α] {s : set α} {x : α} :

s.nonempty → (x ∈ closure s ↔ metric.inf_dist x s = 0)

A point belongs to the closure of s iff its infimum distance to this set vanishes

source

theorem metric.mem_iff_inf_dist_zero_of_closed {α : Type u} [metric_space α] {s : set α} {x : α} :

is_closed s → s.nonempty → (x ∈ s ↔ metric.inf_dist x s = 0)

Given a closed set s, a point belongs to s iff its infimum distance to this set vanishes

source

theorem metric.inf_dist_image {α : Type u} {β : Type v} [metric_space α] [metric_space β] {t : set α} {x : α} {Φ : α → β} :

isometry Φ → metric.inf_dist (Φ x) (Φ '' t) = metric.inf_dist x t

The infimum distance is invariant under isometries

source

def metric.Hausdorff_dist {α : Type u} [metric_space α] :

set α → set α → ℝ

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

Equations

metric.Hausdorff_dist s t = (emetric.Hausdorff_edist s t).to_real

source

theorem metric.Hausdorff_dist_nonneg {α : Type u} [metric_space α] {s t : set α} :

0 ≤ metric.Hausdorff_dist s t

The Hausdorff distance is nonnegative

source

theorem metric.Hausdorff_edist_ne_top_of_nonempty_of_bounded {α : Type u} [metric_space α] {s t : set α} :

s.nonempty → t.nonempty → metric.bounded s → metric.bounded t → emetric.Hausdorff_edist s t ≠ ⊤

If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance

source

@[simp]

theorem metric.Hausdorff_dist_self_zero {α : Type u} [metric_space α] {s : set α} :

metric.Hausdorff_dist s s = 0

The Hausdorff distance between a set and itself is zero

source

theorem metric.Hausdorff_dist_comm {α : Type u} [metric_space α] {s t : set α} :

metric.Hausdorff_dist s t = metric.Hausdorff_dist t s

The Hausdorff distance from s to t and from t to s coincide

source

@[simp]

theorem metric.Hausdorff_dist_empty {α : Type u} [metric_space α] {s : set α} :

metric.Hausdorff_dist s ∅ = 0

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use Hausdorff_edist, which takes values in ennreal)

source

@[simp]

theorem metric.Hausdorff_dist_empty' {α : Type u} [metric_space α] {s : set α} :

metric.Hausdorff_dist ∅ s = 0

The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable value ∞ instead, use Hausdorff_edist, which takes values in ennreal)

source

theorem metric.Hausdorff_dist_le_of_inf_dist {α : Type u} [metric_space α] {s t : set α} {r : ℝ} :

0 ≤ r → (∀ (x : α), x ∈ s → metric.inf_dist x t ≤ r) → (∀ (x : α), x ∈ t → metric.inf_dist x s ≤ r) → metric.Hausdorff_dist s t ≤ r

Bounding the Hausdorff distance by bounding the distance of any point in each set to the other set

source

theorem metric.Hausdorff_dist_le_of_mem_dist {α : Type u} [metric_space α] {s t : set α} {r : ℝ} :

0 ≤ r → (∀ (x : α), x ∈ s → (∃ (y : α) (H : y ∈ t), has_dist.dist x y ≤ r)) → (∀ (x : α), x ∈ t → (∃ (y : α) (H : y ∈ s), has_dist.dist x y ≤ r)) → metric.Hausdorff_dist s t ≤ r

Bounding the Hausdorff distance by exhibiting, for any point in each set, another point in the other set at controlled distance

source

theorem metric.Hausdorff_dist_le_diam {α : Type u} [metric_space α] {s t : set α} :

s.nonempty → metric.bounded s → t.nonempty → metric.bounded t → metric.Hausdorff_dist s t ≤ metric.diam (s ∪ t)

The Hausdorff distance is controlled by the diameter of the union

source

theorem metric.inf_dist_le_Hausdorff_dist_of_mem {α : Type u} [metric_space α] {s t : set α} {x : α} :

x ∈ s → emetric.Hausdorff_edist s t ≠ ⊤ → metric.inf_dist x t ≤ metric.Hausdorff_dist s t

The distance to a set is controlled by the Hausdorff distance

source

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt {α : Type u} [metric_space α] {s t : set α} {x : α} {r : ℝ} :

x ∈ s → metric.Hausdorff_dist s t < r → emetric.Hausdorff_edist s t ≠ ⊤ → (∃ (y : α) (H : y ∈ t), has_dist.dist x y < r)

If the Hausdorff distance is <r, then any point in one of the sets is at distance <r of a point in the other set

source

theorem metric.exists_dist_lt_of_Hausdorff_dist_lt' {α : Type u} [metric_space α] {s t : set α} {y : α} {r : ℝ} :

y ∈ t → metric.Hausdorff_dist s t < r → emetric.Hausdorff_edist s t ≠ ⊤ → (∃ (x : α) (H : x ∈ s), has_dist.dist x y < r)

If the Hausdorff distance is <r, then any point in one of the sets is at distance <r of a point in the other set

source

theorem metric.inf_dist_le_inf_dist_add_Hausdorff_dist {α : Type u} [metric_space α] {s t : set α} {x : α} :

emetric.Hausdorff_edist s t ≠ ⊤ → metric.inf_dist x t ≤ metric.inf_dist x s + metric.Hausdorff_dist s t

The infimum distance to s and t are the same, up to the Hausdorff distance between s and t

source

theorem metric.Hausdorff_dist_image {α : Type u} {β : Type v} [metric_space α] [metric_space β] {s t : set α} {Φ : α → β} :

isometry Φ → metric.Hausdorff_dist (Φ '' s) (Φ '' t) = metric.Hausdorff_dist s t

The Hausdorff distance is invariant under isometries

source

theorem metric.Hausdorff_dist_triangle {α : Type u} [metric_space α] {s t u : set α} :

emetric.Hausdorff_edist s t ≠ ⊤ → metric.Hausdorff_dist s u ≤ metric.Hausdorff_dist s t + metric.Hausdorff_dist t u

The Hausdorff distance satisfies the triangular inequality

source

theorem metric.Hausdorff_dist_triangle' {α : Type u} [metric_space α] {s t u : set α} :

emetric.Hausdorff_edist t u ≠ ⊤ → metric.Hausdorff_dist s u ≤ metric.Hausdorff_dist s t + metric.Hausdorff_dist t u

The Hausdorff distance satisfies the triangular inequality

source

@[simp]

theorem metric.Hausdorff_dist_self_closure {α : Type u} [metric_space α] {s : set α} :

metric.Hausdorff_dist s (closure s) = 0

The Hausdorff distance between a set and its closure vanish

source

@[simp]

theorem metric.Hausdorff_dist_closure₁ {α : Type u} [metric_space α] {s t : set α} :

metric.Hausdorff_dist (closure s) t = metric.Hausdorff_dist s t

Replacing a set by its closure does not change the Hausdorff distance.

source

@[simp]

theorem metric.Hausdorff_dist_closure₂ {α : Type u} [metric_space α] {s t : set α} :

metric.Hausdorff_dist s (closure t) = metric.Hausdorff_dist s t

Replacing a set by its closure does not change the Hausdorff distance.

source

@[simp]

theorem metric.Hausdorff_dist_closure {α : Type u} [metric_space α] {s t : set α} :

metric.Hausdorff_dist (closure s) (closure t) = metric.Hausdorff_dist s t

The Hausdorff distance between two sets and their closures coincide

source

theorem metric.Hausdorff_dist_zero_iff_closure_eq_closure {α : Type u} [metric_space α] {s t : set α} :

emetric.Hausdorff_edist s t ≠ ⊤ → (metric.Hausdorff_dist s t = 0 ↔ closure s = closure t)

Two sets are at zero Hausdorff distance if and only if they have the same closures

source

theorem metric.Hausdorff_dist_zero_iff_eq_of_closed {α : Type u} [metric_space α] {s t : set α} :

is_closed s → is_closed t → emetric.Hausdorff_edist s t ≠ ⊤ → (metric.Hausdorff_dist s t = 0 ↔ s = t)

Two closed sets are at zero Hausdorff distance if and only if they coincide

mathlib documentation

topology.metric_space.hausdorff_distance

Hausdorff distance

Main definitions

General documentation

Additional documentation

Library

mathlib documentation

topology.​metric_space.​hausdorff_distance

Hausdorff distance

Main definitions

General documentation

Additional documentation

Library

topology.metric_space.hausdorff_distance