English
In a normal space with disjoint closed s,t and a ≤ b, there exists a bounded continuous f: X → ℝ such that f equals a on s, equals b on t, and a ≤ f(x) ≤ b for all x.
Русский
При данных s,t и a ≤ b существует ограниченная непрерывная функция f: X → ℝ, такая что f= a на s, f= b на t, и a ≤ f(x) ≤ b для всех x.
LaTeX
$$$\\exists f: X \\to \\mathbb{R},\\quad f|_s = a,\\ f|_t = b,\\ \\forall x, f(x) \\in [a,b]$$$
Lean4
/-- Urysohn's lemma: if `s` and `t` are two disjoint closed sets in a normal topological space `X`,
and `a ≤ b` are two real numbers, then there exists a continuous function `f : X → ℝ` such that
* `f` equals `a` on `s`;
* `f` equals `b` on `t`;
* `a ≤ f x ≤ b` for all `x`.
-/
theorem exists_bounded_mem_Icc_of_closed_of_le {X : Type*} [TopologicalSpace X] [NormalSpace X] {s t : Set X}
(hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) {a b : ℝ} (hle : a ≤ b) :
∃ f : X →ᵇ ℝ, EqOn f (Function.const X a) s ∧ EqOn f (Function.const X b) t ∧ ∀ x, f x ∈ Icc a b :=
let ⟨f, hfs, hft, hf01⟩ := exists_bounded_zero_one_of_closed hs ht hd
⟨BoundedContinuousFunction.const X a + (b - a) • f, fun x hx => by simp [hfs hx], fun x hx => by simp [hft hx],
fun x => ⟨by dsimp; nlinarith [(hf01 x).1], by dsimp; nlinarith [(hf01 x).2]⟩⟩
