# mathlibdocumentation

topology.urysohns_bounded

# 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.continuous_function.bounded imports too many other files.

## Tags #

Urysohn's lemma, normal topological space

theorem exists_bounded_zero_one_of_closed {X : Type u_1} [normal_space X] {s t : set X} (hs : is_closed s) (ht : is_closed t) (hd : t) :
∃ (f : , 0 s 1 t ∀ (x : X), f x 1

Urysohns 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} [normal_space X] {s t : set X} (hs : is_closed s) (ht : is_closed t) (hd : t) {a b : } (hle : a b) :
∃ (f : , a) s b) t ∀ (x : X), f x b

Urysohns 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.