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.ContinuousMap.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 t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) : ∃ (f : BoundedContinuousFunction X ℝ), 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} [TopologicalSpace X] [NormalSpace X] {s 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.