feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thi…

…ckening` (#15641)

* rename `emetric.exists_pos_forall_le_edist` ->
  `emetric.exists_pos_forall_lt_edist`;

  - don't assume that the compact set is nonempty;
  - provide an `nnreal` number instead of an `ennreal`;
  - claim strict inequality;

* add `metric.thickening_mem_nhds_set` and
  `metric.cthickening_mem_nhds_set`;

* move `is_compact.exists_thickening_subset_open` below the
  `cthickening` version, make it clear from the proof that the latter
  implies the former;

* add `metric.has_basis_nhds_set_thickening` and
  `metric.has_basis_nhds_set_cthickening`;

* add `continuous.tendsto_nhds_set`

src/topology/metric_space/hausdorff_distance.lean

@@ -174,15 +174,16 @@ begin
   exact ⟨y, ys, le_antisymm (inf_edist_le_edist_of_mem ys) (by rwa le_inf_edist)⟩
 end
 
-lemma exists_pos_forall_le_edist (hs : is_compact s) (hs' : s.nonempty) (ht : is_closed t)
-  (hst : disjoint s t) :
-  ∃ r, 0 < r ∧ ∀ (x ∈ s) (y ∈ t), r ≤ edist x y :=
+lemma exists_pos_forall_lt_edist (hs : is_compact s) (ht : is_closed t) (hst : disjoint s t) :
+  ∃ r : ℝ≥0, 0 < r ∧ ∀ (x ∈ s) (y ∈ t), (r : ℝ≥0∞) < edist x y :=
 begin
+  rcases s.eq_empty_or_nonempty with rfl|hne, { use 1, simp },
   obtain ⟨x, hx, h⟩ : ∃ x ∈ s, ∀ y ∈ s, inf_edist x t ≤ inf_edist y t :=
-    hs.exists_forall_le hs' continuous_inf_edist.continuous_on,
-  refine ⟨inf_edist x t, pos_iff_ne_zero.2 $ λ H, hst ⟨hx, _⟩, λ y hy, le_inf_edist.1 $ h y hy⟩,
-  rw ←ht.closure_eq,
-  exact mem_closure_iff_inf_edist_zero.2 H,
+    hs.exists_forall_le hne continuous_inf_edist.continuous_on,
+  have : 0 < inf_edist x t,
+    from pos_iff_ne_zero.2 (λ H, hst ⟨hx, (mem_iff_inf_edist_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₀, λ y hy z hz, hr.trans_le $ le_inf_edist.1 (h y hy) z hz⟩
 end
 
 end inf_edist --section
@@ -1016,6 +1017,12 @@ lemma self_subset_cthickening {δ : ℝ} (E : set α) :
   E ⊆ cthickening δ E :=
 subset_closure.trans (closure_subset_cthickening δ E)
 
+lemma thickening_mem_nhds_set (E : set α) {δ : ℝ} (hδ : 0 < δ) : thickening δ E ∈ 𝓝ˢ E :=
+is_open_thickening.mem_nhds_set.2 $ self_subset_thickening hδ E
+
+lemma cthickening_mem_nhds_set (E : set α) {δ : ℝ} (hδ : 0 < δ) : cthickening δ E ∈ 𝓝ˢ E :=
+mem_of_superset (thickening_mem_nhds_set E hδ) (thickening_subset_cthickening _ _)
+
 @[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]
@@ -1040,20 +1047,17 @@ lemma _root_.disjoint.exists_thickenings (hst : disjoint s t) (hs : is_compact s
   (ht : is_closed t) :
   ∃ δ, 0 < δ ∧ disjoint (thickening δ s) (thickening δ t) :=
 begin
-  obtain rfl | hs' := s.eq_empty_or_nonempty,
-  { simp_rw thickening_empty,
-    exact ⟨1, zero_lt_one, empty_disjoint _⟩ },
-  obtain ⟨r, hr, h⟩ := exists_pos_forall_le_edist hs hs' ht hst,
-  refine ⟨(min 1 (r/2)).to_real, to_real_pos (lt_min ennreal.zero_lt_one $ half_pos hr.ne').ne'
-    (min_lt_of_left_lt one_lt_top).ne, _⟩,
+  obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst,
+  refine ⟨r / 2, half_pos (nnreal.coe_pos.2 hr), _⟩,
   rintro z ⟨hzs, hzt⟩,
   rw mem_thickening_iff_exists_edist_lt at hzs hzt,
+  rw [← nnreal.coe_two, ← nnreal.coe_div, ennreal.of_real_coe_nnreal] at hzs hzt,
   obtain ⟨x, hx, hzx⟩ := hzs,
   obtain ⟨y, hy, hzy⟩ := hzt,
-  refine (((h _ hx _ hy).trans $ edist_triangle_left _ _ _).trans_lt $
-    ennreal.add_lt_add hzx hzy).not_le _,
-  rw ←two_mul,
-  exact ennreal.mul_le_of_le_div' (of_real_to_real_le.trans $ min_le_right _ _),
+  refine (h x hx y hy).not_le _,
+  calc edist x y ≤ edist z x + edist z y : edist_triangle_left _ _ _
+  ... ≤ ↑(r / 2) + ↑(r / 2) : add_le_add hzx.le hzy.le
+  ... = r : by rw [← ennreal.coe_add, nnreal.add_halves]
 end
 
 lemma _root_.disjoint.exists_cthickenings (hst : disjoint s t) (hs : is_compact s)
@@ -1065,18 +1069,28 @@ begin
     exact (cthickening_subset_thickening' hδ (half_lt_self hδ) _),
 end
 
-lemma _root_.is_compact.exists_thickening_subset_open (hs : is_compact s) (ht : is_open t)
-  (hst : s ⊆ t) :
-  ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
-(hst.disjoint_compl_right.exists_thickenings hs ht.is_closed_compl).imp $ λ δ h,
-  ⟨h.1, disjoint_compl_right_iff_subset.1 $ h.2.mono_right $ self_subset_thickening h.1 _⟩
-
 lemma _root_.is_compact.exists_cthickening_subset_open (hs : is_compact s) (ht : is_open t)
   (hst : s ⊆ t) :
   ∃ δ, 0 < δ ∧ cthickening δ s ⊆ t :=
 (hst.disjoint_compl_right.exists_cthickenings hs ht.is_closed_compl).imp $ λ δ h,
   ⟨h.1, disjoint_compl_right_iff_subset.1 $ h.2.mono_right $ self_subset_cthickening _⟩
 
+lemma _root_.is_compact.exists_thickening_subset_open (hs : is_compact s) (ht : is_open t)
+  (hst : s ⊆ t) :
+  ∃ δ, 0 < δ ∧ thickening δ s ⊆ t :=
+let ⟨δ, h₀, hδ⟩ := hs.exists_cthickening_subset_open ht hst
+  in ⟨δ, h₀, (thickening_subset_cthickening _ _).trans hδ⟩
+
+lemma has_basis_nhds_set_thickening {K : set α} (hK : is_compact K) :
+  (𝓝ˢ K).has_basis (λ δ : ℝ, 0 < δ) (λ δ, thickening δ K) :=
+(has_basis_nhds_set K).to_has_basis' (λ U hU, hK.exists_thickening_subset_open hU.1 hU.2) $
+  λ _, thickening_mem_nhds_set K
+
+lemma has_basis_nhds_set_cthickening {K : set α} (hK : is_compact K) :
+  (𝓝ˢ K).has_basis (λ δ : ℝ, 0 < δ) (λ δ, cthickening δ K) :=
+(has_basis_nhds_set K).to_has_basis' (λ U hU, hK.exists_cthickening_subset_open hU.1 hU.2) $
+  λ _, cthickening_mem_nhds_set K
+
 lemma cthickening_eq_Inter_cthickening' {δ : ℝ}
   (s : set ℝ) (hsδ : s ⊆ Ioi δ) (hs : ∀ ε, δ < ε → (s ∩ (Ioc δ ε)).nonempty) (E : set α) :
   cthickening δ E = ⋂ ε ∈ s, cthickening ε E :=

src/topology/nhds_set.lean

@@ -26,7 +26,8 @@ Furthermore, we have the following results:
 open set filter
 open_locale topological_space
 
-variables {α : Type*} [topological_space α] {s t s₁ s₂ t₁ t₂ : set α} {x : α}
+variables {α β : Type*} [topological_space α] [topological_space β]
+  {s t s₁ s₂ t₁ t₂ : set α} {x : α}
 
 /-- The filter of neighborhoods of a set in a topological space. -/
 def nhds_set (s : set α) : filter α :=
@@ -73,3 +74,10 @@ by simp only [nhds_set, image_union, Sup_union]
 
 lemma union_mem_nhds_set (h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) : s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂) :=
 by { rw nhds_set_union, exact union_mem_sup h₁ h₂ }
+
+/-- Preimage of a set neighborhood of `t` under a continuous map `f` is a set neighborhood of `s`
+provided that `f` maps `s` to `t`.  -/
+lemma continuous.tendsto_nhds_set {f : α → β} {t : set β} (hf : continuous f)
+  (hst : maps_to f s t) : tendsto f (𝓝ˢ s) (𝓝ˢ t) :=
+((has_basis_nhds_set s).tendsto_iff (has_basis_nhds_set t)).mpr $ λ U hU,
+  ⟨f ⁻¹' U, ⟨hU.1.preimage hf, hst.mono subset.rfl hU.2⟩, λ x, id⟩