From 10a5fc8d68de3171444ff6e3a3a5f684a09e59bd Mon Sep 17 00:00:00 2001 From: Kalle-t30200-lr228 Date: Fri, 5 Nov 2021 18:21:41 +0200 Subject: [PATCH 1/6] feat(topology/metric_space/hausdorff_distance): add definition and lemmas about open thickenings of subsets --- .../metric_space/hausdorff_distance.lean | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 50613568802f1..966486322e46f 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -743,4 +743,75 @@ by simp [(Hausdorff_edist_zero_iff_eq_of_closed hs ht).symm, Hausdorff_dist, ennreal.to_real_eq_zero_iff, fin] end --section + +section thickening + +variables {α : Type u} [pseudo_emetric_space α] + +open emetric + +/-- The (open) `δ`-thickening `thickening δ E` of a subset `E` in a pseudo emetric space consists +of those points that are at distance less than `δ` from some point of `E`. -/ +def thickening (δ : ℝ) (E : set α) : set α := {x : α | inf_edist x E < ennreal.of_real δ} + +/-- The (open) thickening equals the preimage of an open interval under `inf_edist`. -/ +lemma thickening_eq_preimage_inf_edist (δ : ℝ) (E : set α) : + thickening δ E = (λ x, inf_edist x E) ⁻¹' (Iio (ennreal.of_real δ)) := rfl + +/-- The (open) thickening is an open set. -/ +lemma is_open_thickening {δ : ℝ} {E : set α} : is_open (thickening δ E) := +continuous.is_open_preimage continuous_inf_edist _ is_open_Iio + +/-- The (open) thickening of the empty set is empty. -/ +@[simp] lemma thickening_empty (δ : ℝ) : thickening δ (∅ : set α) = ∅ := +by { unfold thickening, simp only [set_of_false, inf_edist_empty, not_top_lt], } + +/-- The (open) thickening `thickening δ E` of a fixed subset `E` is increasing function of the +thickening radius `δ`. -/ +lemma thickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) : + thickening δ₁ E ⊆ thickening δ₂ E := +preimage_mono (Iio_subset_Iio (ennreal.of_real_le_of_real hle)) + +/-- The (open) thickening `thickening δ E` with a fixed thickening radius `δ` is +an increasing function of the subset `E`. -/ +lemma thickening_subset_of_subset (δ : ℝ) {E₁ E₂ : set α} (h : E₁ ⊆ E₂) : + thickening δ E₁ ⊆ thickening δ E₂ := +λ _ hx, lt_of_le_of_lt (inf_edist_le_inf_edist_of_subset h) hx + +variables {X : Type u} [metric_space X] + +/-- A point in a metric space belongs to the (open) `δ`-thickening of a subset `E` if and only if +it is at distance less than `δ` from some point of `E`. -/ +lemma mem_thickening_iff {δ : ℝ} (E : set X) (x : X) : + x ∈ thickening δ E ↔ (∃ z ∈ E, dist x z < δ) := +begin + unfold thickening, + simp, + split, + { intros h, + rcases (exists_edist_lt_of_inf_edist_lt h) with ⟨z , ⟨hzE, hxz⟩⟩, + use z, + split, + { exact hzE, }, + rw dist_edist, + apply (@ennreal.of_real_lt_of_real_iff_of_nonneg + ((edist x z).to_real) δ (ennreal.to_real_nonneg)).mp, + rwa ennreal.of_real_to_real (edist_lt_top x z).ne, }, + { intros h, + rcases h with ⟨z , ⟨hzE, hxz⟩⟩, + rw dist_edist at hxz, + apply lt_of_le_of_lt (@inf_edist_le_edist_of_mem _ _ x _ _ hzE) _, + have key := (@ennreal.of_real_lt_of_real_iff_of_nonneg + ((edist x z).to_real) δ (ennreal.to_real_nonneg)).mpr hxz, + rwa ennreal.of_real_to_real (edist_lt_top x z).ne at key, }, +end + +/-- The (open) `δ`-thickening `thickening δ E` of a subset `E` in a metric space equals the +union of balls of radius `δ` centered at points of `E`. -/ +lemma thickening_eq_bUnion_ball {δ : ℝ} {E : set X} : + thickening δ E = ⋃ x ∈ E, ball x δ := +by { ext x, rw mem_bUnion_iff, exact mem_thickening_iff E x, } + +end thickening --section + end metric --namespace From 697c9557136919a976623ce735df01f753bf4d6c Mon Sep 17 00:00:00 2001 From: kkytola <39528102+kkytola@users.noreply.github.com> Date: Fri, 12 Nov 2021 21:34:29 +0200 Subject: [PATCH 2/6] Apply suggestions from code review Co-authored-by: sgouezel --- src/topology/metric_space/hausdorff_distance.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 966486322e46f..0aeedef50db5b 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -766,7 +766,7 @@ continuous.is_open_preimage continuous_inf_edist _ is_open_Iio @[simp] lemma thickening_empty (δ : ℝ) : thickening δ (∅ : set α) = ∅ := by { unfold thickening, simp only [set_of_false, inf_edist_empty, not_top_lt], } -/-- The (open) thickening `thickening δ E` of a fixed subset `E` is increasing function of the +/-- The (open) thickening `thickening δ E` of a fixed subset `E` is an increasing function of the thickening radius `δ`. -/ lemma thickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) : thickening δ₁ E ⊆ thickening δ₂ E := @@ -789,7 +789,7 @@ begin simp, split, { intros h, - rcases (exists_edist_lt_of_inf_edist_lt h) with ⟨z , ⟨hzE, hxz⟩⟩, + rcases (exists_edist_lt_of_inf_edist_lt h) with ⟨z, ⟨hzE, hxz⟩⟩, use z, split, { exact hzE, }, @@ -798,7 +798,7 @@ begin ((edist x z).to_real) δ (ennreal.to_real_nonneg)).mp, rwa ennreal.of_real_to_real (edist_lt_top x z).ne, }, { intros h, - rcases h with ⟨z , ⟨hzE, hxz⟩⟩, + rcases h with ⟨z, ⟨hzE, hxz⟩⟩, rw dist_edist at hxz, apply lt_of_le_of_lt (@inf_edist_le_edist_of_mem _ _ x _ _ hzE) _, have key := (@ennreal.of_real_lt_of_real_iff_of_nonneg From 9d5a57b8f488c258beb39ef4e6ef6ee1badf95c7 Mon Sep 17 00:00:00 2001 From: Kalle-t30200-lr228 Date: Fri, 12 Nov 2021 21:51:59 +0200 Subject: [PATCH 3/6] Changes as suggested in review. --- src/topology/metric_space/hausdorff_distance.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 0aeedef50db5b..26051425f90b9 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -23,7 +23,8 @@ This files introduces: * `inf_edist x s`, the infimum edistance of a point `x` to a set `s` in an emetric space * `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space * Versions of these notions on metric spaces, called respectively `inf_dist` and -`Hausdorff_dist`. +`Hausdorff_dist`, +* `thickening δ s`, the open thickening by radius `δ` os a set `s` in a pseudo emetric space. -/ noncomputable theory open_locale classical nnreal ennreal topological_space @@ -786,13 +787,11 @@ lemma mem_thickening_iff {δ : ℝ} (E : set X) (x : X) : x ∈ thickening δ E ↔ (∃ z ∈ E, dist x z < δ) := begin unfold thickening, - simp, + simp only [exists_prop, mem_set_of_eq], split, { intros h, rcases (exists_edist_lt_of_inf_edist_lt h) with ⟨z, ⟨hzE, hxz⟩⟩, - use z, - split, - { exact hzE, }, + refine ⟨z, hzE, _⟩, rw dist_edist, apply (@ennreal.of_real_lt_of_real_iff_of_nonneg ((edist x z).to_real) δ (ennreal.to_real_nonneg)).mp, From 9520db71ee2c817adf059426c81a58d369bacd51 Mon Sep 17 00:00:00 2001 From: Kalle-t30200-lr228 Date: Fri, 12 Nov 2021 21:58:17 +0200 Subject: [PATCH 4/6] Correcting a misprint in the docstring. --- src/topology/metric_space/hausdorff_distance.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 26051425f90b9..11ebd88916f13 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -24,7 +24,7 @@ This files introduces: * `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space * Versions of these notions on metric spaces, called respectively `inf_dist` and `Hausdorff_dist`, -* `thickening δ s`, the open thickening by radius `δ` os a set `s` in a pseudo emetric space. +* `thickening δ s`, the open thickening by radius `δ` of a set `s` in a pseudo emetric space. -/ noncomputable theory open_locale classical nnreal ennreal topological_space From 3704bf5182ff9b06d431c734a40ecea535fb0e62 Mon Sep 17 00:00:00 2001 From: kkytola <39528102+kkytola@users.noreply.github.com> Date: Tue, 16 Nov 2021 08:52:53 +0200 Subject: [PATCH 5/6] Update src/topology/metric_space/hausdorff_distance.lean Co-authored-by: sgouezel --- src/topology/metric_space/hausdorff_distance.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 11ebd88916f13..515e45b3f0626 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -765,7 +765,7 @@ continuous.is_open_preimage continuous_inf_edist _ is_open_Iio /-- The (open) thickening of the empty set is empty. -/ @[simp] lemma thickening_empty (δ : ℝ) : thickening δ (∅ : set α) = ∅ := -by { unfold thickening, simp only [set_of_false, inf_edist_empty, not_top_lt], } +by simp only [thickening, set_of_false, inf_edist_empty, not_top_lt] /-- The (open) thickening `thickening δ E` of a fixed subset `E` is an increasing function of the thickening radius `δ`. -/ From afbecced3d83cb7ff4b1781f20fb4615551aa4b3 Mon Sep 17 00:00:00 2001 From: Kalle-swift Date: Tue, 16 Nov 2021 09:01:58 +0200 Subject: [PATCH 6/6] Removed a comma in a docstring. --- src/topology/metric_space/hausdorff_distance.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index 515e45b3f0626..fe3058078c4c3 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/src/topology/metric_space/hausdorff_distance.lean @@ -22,8 +22,7 @@ expressed in the setting of emetric spaces. This files introduces: * `inf_edist x s`, the infimum edistance of a point `x` to a set `s` in an emetric space * `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space -* Versions of these notions on metric spaces, called respectively `inf_dist` and -`Hausdorff_dist`, +* Versions of these notions on metric spaces, called respectively `inf_dist` and `Hausdorff_dist` * `thickening δ s`, the open thickening by radius `δ` of a set `s` in a pseudo emetric space. -/ noncomputable theory