From 0bcd6be6b061f4b3465ad878329e8af982ebb987 Mon Sep 17 00:00:00 2001 From: grunweg Date: Sat, 27 Jan 2024 17:21:40 +0000 Subject: [PATCH] feat: two lemmas about cut-off functions (#9873) From sphere-eversion; I'm just upstreaming this. The version in sphere-eversion uses an unbundled design; we provide a bundled version (for now) to match the remaining file. Co-authored-by: grunweg --- .../Geometry/Manifold/PartitionOfUnity.lean | 31 ++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean index 0a1216e338a1e..404fcaafb44de 100644 --- a/Mathlib/Geometry/Manifold/PartitionOfUnity.lean +++ b/Mathlib/Geometry/Manifold/PartitionOfUnity.lean @@ -483,7 +483,7 @@ See also `exists_msmooth_zero_iff_one_iff_of_isClosed`, which ensures additional `f` is equal to `0` exactly on `s` and to `1` exactly on `t`. -/ theorem exists_smooth_zero_one_of_isClosed [T2Space M] [SigmaCompactSpace M] {s t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : - ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by + ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc 0 1 := by have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx) rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩ set g := f.toSmoothPartitionOfUnity @@ -495,6 +495,35 @@ theorem exists_smooth_zero_one_of_isClosed [T2Space M] [SigmaCompactSpace M] {s exact nmem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx) #align exists_smooth_zero_one_of_closed exists_smooth_zero_one_of_isClosed +/-- Given two disjoint closed sets `s, t` in a Hausdorff normal σ-compact finite dimensional +manifold `M`, there exists a smooth function `f : M → [0,1]` that vanishes in a neighbourhood of `s` +and is equal to `1` in a neighbourhood of `t`. -/ +theorem exists_smooth_zero_one_nhds_of_isClosed [T2Space M] [NormalSpace M] [SigmaCompactSpace M] + {s t : Set M} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : + ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, (∀ᶠ x in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ x in 𝓝ˢ t, f x = 1) ∧ + ∀ x, f x ∈ Icc 0 1 := by + obtain ⟨u, u_op, hsu, hut⟩ := normal_exists_closure_subset hs ht.isOpen_compl + (subset_compl_iff_disjoint_left.mpr hd.symm) + obtain ⟨v, v_op, htv, hvu⟩ := normal_exists_closure_subset ht isClosed_closure.isOpen_compl + (subset_compl_comm.mp hut) + obtain ⟨f, hfu, hfv, hf⟩ := exists_smooth_zero_one_of_isClosed I isClosed_closure isClosed_closure + (subset_compl_iff_disjoint_left.mp hvu) + refine ⟨f, ?_, ?_, hf⟩ + · exact eventually_of_mem (mem_of_superset (u_op.mem_nhdsSet.mpr hsu) subset_closure) hfu + · exact eventually_of_mem (mem_of_superset (v_op.mem_nhdsSet.mpr htv) subset_closure) hfv + +/-- Given two sets `s, t` in a Hausdorff normal σ-compact finite-dimensional manifold `M` +with `s` open and `s ⊆ interior t`, there is a smooth function `f : M → [0,1]` which is equal to `s` +in a neighbourhood of `s` and has support contained in `t`. -/ +theorem exists_smooth_one_nhds_of_subset_interior [T2Space M] [NormalSpace M] [SigmaCompactSpace M] + {s t : Set M} (hs : IsClosed s) (hd : s ⊆ interior t) : + ∃ f : C^∞⟮I, M; 𝓘(ℝ), ℝ⟯, (∀ᶠ x in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ + ∀ x, f x ∈ Icc 0 1 := by + rcases exists_smooth_zero_one_nhds_of_isClosed I isOpen_interior.isClosed_compl hs + (by rwa [← subset_compl_iff_disjoint_left, compl_compl]) with ⟨f, h0, h1, hf⟩ + refine ⟨f, h1, fun x hx ↦ ?_, hf⟩ + exact h0.self_of_nhdsSet _ fun hx' ↦ hx <| interior_subset hx' + namespace SmoothPartitionOfUnity /-- A `SmoothPartitionOfUnity` that consists of a single function, uniformly equal to one,