English
In a T2 space, for open s with compact closure and closed t with t ⊆ s, there exists a continuous f supported in s with f = 1 on t and 0 ≤ f ≤ 1.
Русский
В пространстве T2 для открытого s с компактной замыканием и замкнутого t, удовлетворяющего t ⊆ s, существует непрерывная f с опорой в s, такая что f = 1 на t и 0 ≤ f ≤ 1.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), \operatorname{tsupport} f \subseteq s, f|_t = 1, ∀ x, f(x) \in Icc(0,1)$$$
Lean4
/-- 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`. -/
theorem 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, hDisjointuv⟩ :=
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 hDisjointuv
have huvc : closure u ⊆ vᶜ := closure_minimal hDisjointuv hvIsOpen.isClosed_compl
let P : Set X → Set X → Prop := fun C _ => sᶜ ⊆ C
set c : Urysohns.CU P :=
{ C := closure u
U := tᶜ
P_C_U := 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, (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_notMem_U
exact notMem_compl_iff.mpr hx
