# Documentation

Mathlib.Topology.UrysohnsBounded

# Urysohn's lemma for bounded continuous functions #

In this file we reformulate Urysohn's lemma exists_continuous_zero_one_of_closed in terms of bounded continuous functions X →ᵇ ℝ. These lemmas live in a separate file because Topology.ContinuousFunction.Bounded imports too many other files.

## Tags #

Urysohn's lemma, normal topological space

theorem exists_bounded_zero_one_of_closed {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hd : Disjoint s t) :
f, Set.EqOn (f) 0 s Set.EqOn (f) 1 t ∀ (x : X), f x Set.Icc 0 1

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_mem_Icc_of_closed_of_le {X : Type u_1} [] [] {s : Set X} {t : Set X} (hs : ) (ht : ) (hd : Disjoint s t) {a : } {b : } (hle : a b) :
f, Set.EqOn (f) () s Set.EqOn (f) () t ∀ (x : X), f x Set.Icc a b

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.