English
Variant where the function is 1 on s, 0 on t, compact support, and 0 ≤ f ≤ 1.
Русский
Вариант, где f равно 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 compactly supported
function `f : X → ℝ` such that
* `f` equals one on `s`;
* `f` equals zero on `t`;
* `0 ≤ f x ≤ 1` for all `x`.
-/
theorem exists_continuous_one_zero_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 1 s ∧ EqOn f 0 t ∧ HasCompactSupport f ∧ ∀ 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
rcases
exists_continuous_zero_one_of_isCompact hs isOpen_interior.isClosed_compl
(disjoint_compl_right_iff_subset.mpr sk) with
⟨⟨f, hf⟩, hfs, hft, h'f⟩
have A : t ⊆ (interior k)ᶜ := subset_compl_comm.mpr (interior_subset.trans kt)
refine
⟨⟨fun x ↦ 1 - f x, continuous_const.sub hf⟩, fun x hx ↦ by simpa using hfs hx, fun x hx ↦ by
simpa [sub_eq_zero] using (hft (A hx)).symm, ?_, fun x ↦ ?_⟩
· apply HasCompactSupport.intro' k_comp k_closed (fun x hx ↦ ?_)
simp only [ContinuousMap.coe_mk, sub_eq_zero]
apply (hft _).symm
contrapose! hx
simp only [mem_compl_iff, not_not] at hx
exact interior_subset hx
· have : 0 ≤ f x ∧ f x ≤ 1 := by simpa using h'f x
simp [this]
