From 65d8b84e11284e7906c8d70da846a1132795055e Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 26 Jul 2022 11:31:04 +0000 Subject: [PATCH] feat(tooplogy/metric_space/hausdorff_distance): add lemmas about `thickening` (#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` --- .../metric_space/hausdorff_distance.lean | 60 ++++++++++++------- src/topology/nhds_set.lean | 10 +++- 2 files changed, 46 insertions(+), 24 deletions(-) diff --git a/src/topology/metric_space/hausdorff_distance.lean b/src/topology/metric_space/hausdorff_distance.lean index b0bc756d86604..1e59651bbb2e9 100644 --- a/src/topology/metric_space/hausdorff_distance.lean +++ b/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 := diff --git a/src/topology/nhds_set.lean b/src/topology/nhds_set.lean index 9a215090a215b..23a632815070e 100644 --- a/src/topology/nhds_set.lean +++ b/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⟩