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}
[topological_space X]
[normal_space X]
{s t : set X}
(hs : is_closed s)
(ht : is_closed t)
(hd : disjoint s t) :
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 ons
;f
equals one ont
;0 ≤ f x ≤ 1
for allx
.
theorem
exists_bounded_mem_Icc_of_closed_of_le
{X : Type u_1}
[topological_space X]
[normal_space X]
{s t : set X}
(hs : is_closed s)
(ht : is_closed t)
(hd : disjoint s t)
{a b : ℝ}
(hle : a ≤ b) :
∃ (f : bounded_continuous_function X ℝ), set.eq_on ⇑f (function.const X a) s ∧ set.eq_on ⇑f (function.const X b) t ∧ ∀ (x : X), ⇑f x ∈ set.Icc a 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
equalsa
ons
;f
equalsb
ont
;a ≤ f x ≤ b
for allx
.