mathlib documentation

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} [topological_space X] [normal_space X] {s t : set X} (hs : is_closed s) (ht : is_closed t) (hd : disjoint s t) :
∃ (f : 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.
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 : 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.