English
Urysohns lemma variant: for regular locally compact spaces with compact s, closed t disjoint from s, there exists f with f = 0 on t and f = 1 on s, with 0 ≤ f ≤ 1 and compact support.
Русский
В нормальном локально компактном пространстве существует функция с поддержкой компактной области, равная 1 на компактном s и 0 на t, с ограничениями 0 ≤ f ≤ 1.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), f|_s = 1, f|_t = 0, HasCompactSupport f, \forall x\; f(x) \in Icc(0,1)$$$
Lean4
/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
space `X`, with `s` compact and `t` closed, then there exists a continuous
function `f : X → ℝ` such that
* `f` equals zero on `s`;
* `f` equals one on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
-/
theorem exists_continuous_zero_one_of_isCompact [RegularSpace X] [LocallyCompactSpace X] {s t : Set X}
(hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
∃ f : C(X, ℝ), EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
by
obtain ⟨k, k_comp, k_closed, sk, kt⟩ : ∃ k, IsCompact k ∧ IsClosed k ∧ s ⊆ interior k ∧ k ⊆ tᶜ :=
exists_compact_closed_between hs ht.isOpen_compl hd.symm.subset_compl_left
let P : Set X → Set X → Prop := fun C _ => IsCompact C
set c : Urysohns.CU P :=
{ C := k
U := tᶜ
P_C_U := k_comp
closed_C := k_closed
open_U := ht.isOpen_compl
subset := kt
hP := by
rintro c u - c_comp u_open cu
rcases exists_compact_closed_between c_comp u_open cu with ⟨k, k_comp, k_closed, ck, ku⟩
have A : closure (interior k) ⊆ k := (IsClosed.closure_subset_iff k_closed).2 interior_subset
refine ⟨interior k, isOpen_interior, ck, A.trans ku, c_comp, k_comp.of_isClosed_subset isClosed_closure A⟩ }
exact
⟨⟨c.lim, c.continuous_lim⟩, fun x hx ↦ c.lim_of_mem_C _ (sk.trans interior_subset hx), fun x hx =>
c.lim_of_notMem_U _ fun h => h hx, c.lim_mem_Icc⟩
