# Urysohn's lemma for bounded continuous functions #

In this file we reformulate Urysohn's lemma `exists_continuous_zero_one_of_isClosed`

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}
[TopologicalSpace X]
[NormalSpace X]
{s : Set X}
{t : Set X}
(hs : IsClosed s)
(ht : IsClosed t)
(hd : Disjoint s t)
:

**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}
[TopologicalSpace X]
[NormalSpace X]
{s : Set X}
{t : Set X}
(hs : IsClosed s)
(ht : IsClosed t)
(hd : Disjoint s t)
{a : ℝ}
{b : ℝ}
(hle : a ≤ b)
:

∃ (f : BoundedContinuousFunction X ℝ),
Set.EqOn (⇑f) (Function.const X a) s ∧ Set.EqOn (⇑f) (Function.const X b) 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`

.