feat(topology/metric_space/hausdorff_distance): Thickening the closure (

#13515)

`thickening δ (closure s) = thickening δ s` and other simple lemmas. Also rename `inf_edist_le_inf_edist_of_subset` to `inf_edist_anti` and make arguments to `mem_thickening_iff` implicit.

src/data/real/ennreal.lean

@@ -1559,6 +1559,8 @@ by simp [ennreal.of_real]
 @[simp] lemma zero_eq_of_real {p : ℝ} : 0 = ennreal.of_real p ↔ p ≤ 0 :=
 eq_comm.trans of_real_eq_zero
 
+alias ennreal.of_real_eq_zero ↔ _ ennreal.of_real_of_nonpos
+
 lemma of_real_le_iff_le_to_real {a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ∞) :
   ennreal.of_real a ≤ b ↔ a ≤ ennreal.to_real b :=
 begin

src/data/set/lattice.lean

@@ -1649,3 +1649,13 @@ noncomputable def Union_eq_sigma_of_disjoint {t : α → set β}
 (equiv.of_bijective _ $ sigma_to_Union_bijective t h).symm
 
 end set
+
+open set
+
+variables [complete_lattice β]
+
+lemma supr_Union (s : ι → set α) (f : α → β) : (⨆ a ∈ (⋃ i, s i), f a) = ⨆ i (a ∈ s i), f a :=
+by { rw supr_comm, simp_rw [mem_Union, supr_exists] }
+
+lemma infi_Union (s : ι → set α) (f : α → β) : (⨅ a ∈ (⋃ i, s i), f a) = ⨅ i (a ∈ s i), f a :=
+by { rw infi_comm, simp_rw [mem_Union, infi_exists] }

src/topology/metric_space/hausdorff_distance.lean

@@ -32,12 +32,13 @@ universes u v w
 
 open classical set function topological_space filter
 
+variables {ι : Sort*} {α : Type u} {β : Type v}
+
 namespace emetric
 
 section inf_edist
 
-variables {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β] {x y : α}
-{s t : set α} {Φ : α → β}
+variables [pseudo_emetric_space α] [pseudo_emetric_space β] {x y : α} {s t : set α} {Φ : α → β}
 
 /-! ### Distance of a point to a set as a function into `ℝ≥0∞`. -/
 
@@ -53,6 +54,10 @@ by simp only [inf_edist, le_infi_iff]
 @[simp] lemma inf_edist_union : inf_edist x (s ∪ t) = inf_edist x s ⊓ inf_edist x t :=
 infi_union
 
+@[simp] lemma inf_edist_Union (f : ι → set α) (x : α) :
+  inf_edist x (⋃ i, f i) = ⨅ i, inf_edist x (f i) :=
+infi_Union f _
+
 /-- The edist to a singleton is the edistance to the single point of this singleton -/
 @[simp] lemma inf_edist_singleton : inf_edist x {y} = edist x y :=
 infi_singleton
@@ -64,9 +69,8 @@ lemma inf_edist_le_edist_of_mem (h : y ∈ s) : inf_edist x s ≤ edist x y := i
 lemma inf_edist_zero_of_mem (h : x ∈ s) : inf_edist x s = 0 :=
 nonpos_iff_eq_zero.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
 
-/-- The edist is monotonous with respect to inclusion -/
-lemma inf_edist_le_inf_edist_of_subset (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s :=
-infi_le_infi_of_subset h
+/-- The edist is antitone with respect to inclusion. -/
+lemma inf_edist_anti (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s := infi_le_infi_of_subset h
 
 /-- The edist to a set is `< r` iff there exists a point in the set at edistance `< r` -/
 lemma inf_edist_lt_iff {r : ℝ≥0∞} : inf_edist x s < r ↔ ∃ y ∈ s, edist x y < r :=
@@ -79,6 +83,9 @@ calc (⨅ z ∈ s, edist x z) ≤ ⨅ z ∈ s, edist y z + edist x y :
   infi₂_mono $ λ z hz, (edist_triangle _ _ _).trans_eq (add_comm _ _)
 ... = (⨅ z ∈ s, edist y z) + edist x y : by simp only [ennreal.infi_add]
 
+lemma inf_edist_le_edist_add_inf_edist : inf_edist x s ≤ edist x y + inf_edist y s :=
+by { rw add_comm, exact inf_edist_le_inf_edist_add_edist }
+
 /-- The edist to a set depends continuously on the point -/
 @[continuity]
 lemma continuous_inf_edist : continuous (λx, inf_edist x s) :=
@@ -88,7 +95,7 @@ continuous_of_le_add_edist 1 (by simp) $
 /-- The edist to a set and to its closure coincide -/
 lemma inf_edist_closure : inf_edist x (closure s) = inf_edist x s :=
 begin
-  refine le_antisymm (inf_edist_le_inf_edist_of_subset subset_closure) _,
+  refine le_antisymm (inf_edist_anti subset_closure) _,
   refine ennreal.le_of_forall_pos_le_add (λε εpos h, _),
   have ε0 : 0 < (ε / 2 : ℝ≥0∞) := by simpa [pos_iff_ne_zero] using εpos,
   have : inf_edist x (closure s) < inf_edist x (closure s) + ε/2,
@@ -182,8 +189,7 @@ by rw Hausdorff_edist
 
 section Hausdorff_edist
 
-variables {α : Type u} {β : Type v} [pseudo_emetric_space α] [pseudo_emetric_space β]
-          {x y : α} {s t u : set α} {Φ : α → β}
+variables [pseudo_emetric_space α] [pseudo_emetric_space β] {x y : α} {s t u : set α} {Φ : α → β}
 
 /-- The Hausdorff edistance of a set to itself vanishes -/
 @[simp] lemma Hausdorff_edist_self : Hausdorff_edist s s = 0 :=
@@ -370,8 +376,7 @@ modulo some tedious rewriting of inequalities from one to the other. -/
 
 namespace metric
 section
-variables {α : Type u} {β : Type v} [pseudo_metric_space α] [pseudo_metric_space β]
-  {s t u : set α} {x y : α} {Φ : α → β}
+variables [pseudo_metric_space α] [pseudo_metric_space β] {s t u : set α} {x y : α} {Φ : α → β}
 open emetric
 
 /-! ### Distance of a point to a set as a function into `ℝ`. -/
@@ -418,7 +423,7 @@ lemma inf_dist_le_inf_dist_of_subset (h : s ⊆ t) (hs : s.nonempty) :
 begin
   have ht : t.nonempty := hs.mono h,
   rw [inf_dist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ht) (inf_edist_ne_top hs)],
-  exact inf_edist_le_inf_edist_of_subset h
+  exact inf_edist_anti h
 end
 
 /-- The minimal distance to a set is `< r` iff there exists a point in this set at distance `< r` -/
@@ -787,14 +792,17 @@ end --section
 
 section thickening
 
-variables {α : Type u} [pseudo_emetric_space α]
+variables [pseudo_emetric_space α] {δ : ℝ} {s : set α} {x : α}
 
 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 δ}
 
+lemma mem_thickening_iff_inf_edist_lt : x ∈ thickening δ s ↔ inf_edist x s < ennreal.of_real δ :=
+iff.rfl
+
 /-- 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
@@ -807,6 +815,9 @@ continuous.is_open_preimage continuous_inf_edist _ is_open_Iio
 @[simp] lemma thickening_empty (δ : ℝ) : thickening δ (∅ : set α) = ∅ :=
 by simp only [thickening, set_of_false, inf_edist_empty, not_top_lt]
 
+lemma thickening_of_nonpos (hδ : δ ≤ 0) (s : set α) : thickening δ s = ∅ :=
+eq_empty_of_forall_not_mem $ λ x, ((ennreal.of_real_of_nonpos hδ).trans_le bot_le).not_lt
+
 /-- The (open) thickening `thickening δ E` of a fixed subset `E` is an increasing function of the
 thickening radius `δ`. -/
 lemma thickening_mono {δ₁ δ₂ : ℝ} (hle : δ₁ ≤ δ₂) (E : set α) :
@@ -817,7 +828,7 @@ preimage_mono (Iio_subset_Iio (ennreal.of_real_le_of_real hle))
 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
+λ _ hx, lt_of_le_of_lt (inf_edist_anti h) hx
 
 lemma mem_thickening_iff_exists_edist_lt {δ : ℝ} (E : set α) (x : α) :
   x ∈ thickening δ E ↔ ∃ z ∈ E, edist x z < ennreal.of_real δ :=
@@ -827,7 +838,7 @@ variables {X : Type u} [pseudo_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) :
+lemma mem_thickening_iff {E : set X} {x : X} :
   x ∈ thickening δ E ↔ (∃ z ∈ E, dist x z < δ) :=
 begin
   have key_iff : ∀ (z : X), edist x z < ennreal.of_real δ ↔ dist x z < δ,
@@ -848,7 +859,7 @@ by { ext, simp [mem_thickening_iff] }
 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_Union₂, exact mem_thickening_iff E x, }
+by { ext x, rw mem_Union₂, exact mem_thickening_iff }
 
 lemma bounded.thickening {δ : ℝ} {E : set X} (h : bounded E) :
   bounded (thickening δ E) :=
@@ -857,7 +868,7 @@ begin
   rcases h.subset_ball x with ⟨R, hR⟩,
   refine (bounded_iff_subset_ball x).2 ⟨R + δ, _⟩,
   assume y hy,
-  rcases (mem_thickening_iff _ _).1 hy with ⟨z, zE, hz⟩,
+  rcases mem_thickening_iff.1 hy with ⟨z, zE, hz⟩,
   calc dist y x ≤ dist z x + dist y z : by { rw add_comm, exact dist_triangle _ _ _ }
   ... ≤ R + δ : add_le_add (hR zE) hz.le
 end
@@ -866,14 +877,17 @@ end thickening --section
 
 section cthickening
 
-variables {α : Type*} [pseudo_emetric_space α]
+variables [pseudo_emetric_space α] {δ ε : ℝ} {s : set α} {x : α}
 
 open emetric
 
 /-- The closed `δ`-thickening `cthickening δ E` of a subset `E` in a pseudo emetric space consists
 of those points that are at infimum distance at most `δ` from `E`. -/
 def cthickening (δ : ℝ) (E : set α) : set α := {x : α | inf_edist x E ≤ ennreal.of_real δ}
 
+@[simp] lemma mem_cthickening_iff : x ∈ cthickening δ s ↔ inf_edist x s ≤ ennreal.of_real δ :=
+iff.rfl
+
 lemma mem_cthickening_of_edist_le (x y : α) (δ : ℝ) (E : set α) (h : y ∈ E)
   (h' : edist x y ≤ ennreal.of_real δ) :
   x ∈ cthickening δ E :=
@@ -931,7 +945,7 @@ end
 an increasing function of the subset `E`. -/
 lemma cthickening_subset_of_subset (δ : ℝ) {E₁ E₂ : set α} (h : E₁ ⊆ E₂) :
   cthickening δ E₁ ⊆ cthickening δ E₂ :=
-λ _ hx, le_trans (inf_edist_le_inf_edist_of_subset h) hx
+λ _ hx, le_trans (inf_edist_anti h) hx
 
 lemma cthickening_subset_thickening {δ₁ : ℝ≥0} {δ₂ : ℝ} (hlt : (δ₁ : ℝ) < δ₂) (E : set α) :
   cthickening δ₁ E ⊆ thickening δ₂ E :=
@@ -991,6 +1005,24 @@ lemma self_subset_cthickening {δ : ℝ} (E : set α) :
   E ⊆ cthickening δ E :=
 subset_closure.trans (closure_subset_cthickening δ E)
 
+@[simp] lemma thickening_union (δ : ℝ) (s t : set α) :
+  thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t :=
+by simp_rw [thickening, inf_edist_union, inf_eq_min, min_lt_iff, set_of_or]
+
+@[simp] lemma cthickening_union (δ : ℝ) (s t : set α) :
+  cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t :=
+by simp_rw [cthickening, inf_edist_union, inf_eq_min, min_le_iff, set_of_or]
+
+@[simp] lemma thickening_Union (δ : ℝ) (f : ι → set α) :
+  thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i) :=
+by simp_rw [thickening, inf_edist_Union, infi_lt_iff, set_of_exists]
+
+@[simp] lemma thickening_closure : thickening δ (closure s) = thickening δ s :=
+by simp_rw [thickening, inf_edist_closure]
+
+@[simp] lemma cthickening_closure : cthickening δ (closure s) = cthickening δ s :=
+by simp_rw [cthickening, inf_edist_closure]
+
 lemma cthickening_eq_Inter_cthickening' {δ : ℝ}
   (s : set ℝ) (hsδ : s ⊆ Ioi δ) (hs : ∀ ε, δ < ε → (s ∩ (Ioc δ ε)).nonempty) (E : set α) :
   cthickening δ E = ⋂ ε ∈ s, cthickening ε E :=
@@ -1121,6 +1153,22 @@ begin
   exact mem_bUnion yE D2,
 end
 
+lemma inf_edist_le_inf_edist_cthickening_add :
+  inf_edist x s ≤ inf_edist x (cthickening δ s) + ennreal.of_real δ :=
+begin
+  refine le_of_forall_lt' (λ r h, _),
+  simp_rw [←lt_tsub_iff_right, inf_edist_lt_iff, mem_cthickening_iff] at h,
+  obtain ⟨y, hy, hxy⟩ := h,
+  exact inf_edist_le_edist_add_inf_edist.trans_lt ((ennreal.add_lt_add_of_lt_of_le
+    (hy.trans_lt ennreal.of_real_lt_top).ne hxy hy).trans_le
+    (tsub_add_cancel_of_le $ le_self_add.trans (lt_tsub_iff_left.1 hxy).le).le),
+end
+
+lemma inf_edist_le_inf_edist_thickening_add :
+  inf_edist x s ≤ inf_edist x (thickening δ s) + ennreal.of_real δ :=
+inf_edist_le_inf_edist_cthickening_add.trans $
+  add_le_add_right (inf_edist_anti $ thickening_subset_cthickening _ _) _
+
 end cthickening --section
 
 end metric --namespace