Theorems · Theorem · general topology

exists_bounded_mem_Icc_of_closed_of_le

∀ {X : Type u_1} [inst : TopologicalSpace X] [NormalSpace X] {s t : Set X},
  IsClosed s →
    IsClosed t →
      Disjoint s t →
        ∀ {a b : ℝ},
          a ≤ b →
            ∃ f,
              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.

Defined in

Mathlib.Topology.UrysohnsBounded

Cited by

2 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceNormalSpace