feat(Topology/UrysohnsLemma): add a variation of Urysohn's lemma for T2Space (#12459)

prove a version of Urysohn's lemma and separation lemmas needed for them.
- In a `T2Space X`, for a closed set `t` and a relatively compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`, `f x = 1` on `t` and `0 ≤ f x ≤ 1`.

Motivation: this will be used in #12290.

Author: yoh-tanimoto

Mathlib/Topology/Separation.lean

@@ -1410,6 +1410,22 @@ theorem IsCompact.nhdsSet_inter_eq [T2Space X] {s t : Set X} (hs : IsCompact s)
   · exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le
   · exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le
 
+/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, there are open sets `U`,
+`V` that separate `t` and `x`.-/
+lemma IsCompact.separation_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
+    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
+    ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V := by
+  simpa [SeparatedNhds] using SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton
+    isClosed_singleton <| disjoint_singleton_right.mpr H2
+
+/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, `𝓝ˢ t` and `𝓝 x` are
+disjoint. -/
+lemma IsCompact.disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
+    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
+    Disjoint (𝓝ˢ t) (𝓝 x) := by
+  simpa using SeparatedNhds.disjoint_nhdsSet <| .of_isCompact_isCompact_isClosed H1
+    isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2
+
 /-- If a function `f` is
 
 - injective on a compact set `s`;
@@ -1738,6 +1754,25 @@ theorem SeparatedNhds.of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsC
 @[deprecated (since := "2024-01-28")]
 alias separatedNhds_of_isCompact_isCompact := SeparatedNhds.of_isCompact_isCompact
 
+/-- In a `T2Space X`, for disjoint closed sets `s t` such that `closure sᶜ` is compact,
+there are neighbourhoods that separate `s` and `t`.-/
+lemma SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed [T2Space X] {s : Set X}
+    {t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t)
+    (H4 : Disjoint s t) : SeparatedNhds s t := by
+  -- Since `t` is a closed subset of the compact set `closure sᶜ`, it is compact.
+  have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
+  -- we split `s` into its frontier and its interior.
+  rw [← diff_union_of_subset (interior_subset (s := s))]
+  -- since `t ⊆ sᶜ`, which is open, and `interior s` is open, we have
+  -- `SeparatedNhds (interior s) t`, which leaves us only with the frontier.
+  refine .union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
+    H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩
+  -- Since the frontier of `s` is compact (as it is a subset of `closure sᶜ`), we simply apply
+  -- `SeparatedNhds_of_isCompact_isCompact`.
+  rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]
+  refine .of_isCompact_isCompact ?_ ht (disjoint_of_subset_left inter_subset_left H4)
+  exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right
+
 section SeparatedFinset
 
 theorem SeparatedNhds.of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) :

Mathlib/Topology/UrysohnsLemma.lean

@@ -230,6 +230,9 @@ theorem tendsto_approx_atTop (c : CU P) (x : X) :
 theorem lim_of_mem_C (c : CU P) (x : X) (h : x ∈ c.C) : c.lim x = 0 := by
   simp only [CU.lim, approx_of_mem_C, h, ciSup_const]
 
+theorem disjoint_C_support_lim (c : CU P) : Disjoint c.C (Function.support c.lim) :=
+  Function.disjoint_support_iff.mpr (fun x hx => lim_of_mem_C c x hx)
+
 theorem lim_of_nmem_U (c : CU P) (x : X) (h : x ∉ c.U) : c.lim x = 1 := by
   simp only [CU.lim, approx_of_nmem_U c _ h, ciSup_const]
 
@@ -431,6 +434,54 @@ theorem exists_continuous_one_zero_of_isCompact_of_isGδ [RegularSpace X] [Local
   · apply le_trans _ hu.le
     exact tsum_le_tsum (fun n ↦ I n x) (S x) u_sum
 
+/-- A variation of Urysohn's lemma. In a `T2Space X`, for a closed set `t` and a relatively
+compact open set `s` such that `t ⊆ s`, there is a continuous function `f` supported in `s`,
+`f x = 1` on `t` and `0 ≤ f x ≤ 1`. -/
+lemma exists_tsupport_one_of_isOpen_isClosed [T2Space X] {s t : Set X}
+    (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t ⊆ s) : ∃ f : C(X, ℝ),
+    tsupport f ⊆ s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 := by
+-- separate `sᶜ` and `t` by `u` and `v`.
+  rw [← compl_compl s] at hscp
+  obtain ⟨u, v, huIsOpen, hvIsOpen, hscompl_subset_u, ht_subset_v, hDjsjointuv⟩ :=
+    SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed (isClosed_compl_iff.mpr hs)
+    hscp ht (HasSubset.Subset.disjoint_compl_left hst)
+  rw [← subset_compl_iff_disjoint_right] at hDjsjointuv
+  have huvc : closure u ⊆ vᶜ := closure_minimal hDjsjointuv hvIsOpen.isClosed_compl
+-- although `sᶜ` is not compact, `closure s` is compact and we can apply
+-- `SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed`. To apply the condition
+-- recursively, we need to make sure that `sᶜ ⊆ C`.
+  let P : Set X → Prop := fun C => sᶜ ⊆ C
+  set c : Urysohns.CU P :=
+  { C := closure u
+    U := tᶜ
+    P_C := hscompl_subset_u.trans subset_closure
+    closed_C := isClosed_closure
+    open_U := ht.isOpen_compl
+    subset := subset_compl_comm.mp
+      (Subset.trans ht_subset_v (subset_compl_comm.mp huvc))
+    hP := by
+      intro c u0 cIsClosed Pc u0IsOpen csubu0
+      obtain ⟨u1, hu1⟩ := SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed cIsClosed
+        (IsCompact.of_isClosed_subset hscp isClosed_closure
+        (closure_mono (compl_subset_compl.mpr Pc)))
+        (isClosed_compl_iff.mpr u0IsOpen) (HasSubset.Subset.disjoint_compl_right csubu0)
+      simp_rw [← subset_compl_iff_disjoint_right, compl_subset_comm (s := u0)] at hu1
+      obtain ⟨v1, hu1, hv1, hcu1, hv1u, hu1v1⟩ := hu1
+      refine ⟨u1, hu1, hcu1, ?_, (Pc.trans hcu1).trans subset_closure⟩
+      exact closure_minimal hu1v1 hv1.isClosed_compl |>.trans hv1u }
+-- `c.lim = 0` on `closure u` and `c.lim = 1` on `t`, so that `tsupport c.lim ⊆ s`.
+  use ⟨c.lim, c.continuous_lim⟩
+  simp only [ContinuousMap.coe_mk]
+  refine ⟨?_, ?_, Urysohns.CU.lim_mem_Icc c⟩
+  · apply Subset.trans _ (compl_subset_comm.mp hscompl_subset_u)
+    rw [← IsClosed.closure_eq (isClosed_compl_iff.mpr huIsOpen)]
+    apply closure_mono
+    exact Disjoint.subset_compl_right (disjoint_of_subset_right subset_closure
+      (Disjoint.symm (Urysohns.CU.disjoint_C_support_lim c)))
+  · intro x hx
+    apply Urysohns.CU.lim_of_nmem_U
+    exact not_mem_compl_iff.mpr hx
+
 theorem exists_continuous_nonneg_pos [RegularSpace X] [LocallyCompactSpace X] (x : X) :
     ∃ f : C(X, ℝ), HasCompactSupport f ∧ 0 ≤ (f : X → ℝ) ∧ f x ≠ 0 := by
   rcases exists_compact_mem_nhds x with ⟨k, hk, k_mem⟩