Urysohn's lemma for bounded continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

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) :

∃ (f : bounded_continuous_function X ℝ), set.eq_on ⇑f 0 s ∧ set.eq_on ⇑f 1 t ∧ ∀ (x : X), ⇑f x ∈ set.Icc 0 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.

source

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 equals a on s;
f equals b on t;
a ≤ f x ≤ b for all x.