English
Variant of Urysohns lemma in a regular locally compact space: there exists f with f = 0 on t, f = 1 on s, 0 ≤ f ≤ 1, HasCompactSupport.
Русский
В регулярном локально компактном пространстве существует функция, равная 0 на t, 1 на s, удовлетворяющая 0 ≤ f ≤ 1 и компактная поддержка.
LaTeX
$$$\exists f \in C(X, \mathbb{R}), f|_t = 0, f|_s = 1, HasCompactSupport f, ∀ 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 `t`;
* `f` equals one on `s`;
* `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 t ∧ EqOn f 1 s ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
by
obtain ⟨g, hgs, hgt, (hicc : ∀ x, 0 ≤ g x ∧ g x ≤ 1)⟩ := exists_continuous_zero_one_of_isCompact hs ht hd
use 1 - g
refine ⟨?_, ?_, ?_⟩
· intro x hx
simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.zero_apply]
exact sub_eq_zero_of_eq (hgt.symm hx)
· intro x hx
simp only [ContinuousMap.sub_apply, ContinuousMap.one_apply, Pi.one_apply, sub_eq_self]
exact hgs hx
· intro x
simpa [and_comm] using hicc x
