English
In a normal topological space X, for disjoint closed sets s and t there exists a continuous f: X → ℝ with 0 on s, 1 on t, and 0 ≤ f ≤ 1 everywhere.
Русский
В нормальном топологическом пространстве X для непересекающихся замкнутых множеств s и t существует непрерывная функция f: X → ℝ, такая что f=0 на s, f=1 на t и 0 ≤ f ≤ 1 на всей X.
LaTeX
$$$\\exists f: X \\to \\mathbb{R},\\quad f|_s = 0,\\ f|_t = 1,\\ 0 \\le f(x) \\le 1\\ \\forall x$$$
Lean4
/-- **Urysohn's lemma**: if `s` and `t` are two disjoint closed sets in a normal topological
space `X`, 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_bounded_zero_one_of_closed {X : Type*} [TopologicalSpace X] [NormalSpace X] {s t : Set X}
(hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
∃ f : X →ᵇ ℝ, EqOn f 0 s ∧ EqOn f 1 t ∧ ∀ x, f x ∈ Icc (0 : ℝ) 1 :=
let ⟨f, hfs, hft, hf⟩ := exists_continuous_zero_one_of_isClosed hs ht hd
⟨⟨f, 1, fun _ _ => Real.dist_le_of_mem_Icc_01 (hf _) (hf _)⟩, hfs, hft, hf⟩
