Documentation

Mathlib.Topology.UrysohnsLemma

Urysohn's lemma #

In this file we prove Urysohn's lemma exists_continuous_zero_one_of_isClosed: for any two disjoint closed sets s and t in a normal topological space X there exists a continuous function f : X → ℝ such that

We also give versions in a regular locally compact space where one assumes that s is compact and t is closed, in exists_continuous_zero_one_of_isCompact and exists_continuous_one_zero_of_isCompact (the latter providing additionally a function with compact support).

We write a generic proof so that it applies both to normal spaces and to regular locally compact spaces.

Implementation notes #

Most paper sources prove Urysohn's lemma using a family of open sets indexed by dyadic rational numbers on [0, 1]. There are many technical difficulties with formalizing this proof (e.g., one needs to formalize the "dyadic induction", then prove that the resulting family of open sets is monotone). So, we formalize a slightly different proof.

Let Urysohns.CU be the type of pairs (C, U) of a closed set C and an open set U such that CU. Since X is a normal topological space, for each c : CU there exists an open set u such that c.C ⊆ u ∧ closure u ⊆ c.U. We define c.left and c.right to be (c.C, u) and (closure u, c.U), respectively. Then we define a family of functions Urysohns.CU.approx (c : Urysohns.CU) (n : ℕ) : X → ℝ by recursion on n:

For each x this is a monotone family of functions that are equal to zero on c.C and are equal to one outside of c.U. We also have c.approx n x ∈ [0, 1] for all c, n, and x.

Let Urysohns.CU.lim c be the supremum (or equivalently, the limit) of c.approx n. Then properties of Urysohns.CU.approx immediately imply that

In order to prove that c.lim is continuous at x, we prove by induction on n : ℕ that for y in a small neighborhood of x we have |c.lim y - c.lim x| ≤ (3 / 4) ^ n. Induction base follows from c.lim x ∈ [0, 1], c.lim y ∈ [0, 1]. For the induction step, consider two cases:

The actual formalization uses midpoint ℝ x y instead of (x + y) / 2 because we have more API lemmas about midpoint.

Tags #

Urysohn's lemma, normal topological space, locally compact topological space

structure Urysohns.CU {X : Type u_2} [TopologicalSpace X] (P : Set XProp) :
Type u_2

An auxiliary type for the proof of Urysohn's lemma: a pair of a closed set C and its open neighborhood U, together with the assumption that C satisfies the property P C. The latter assumption will make it possible to prove simultaneously both versions of Urysohn's lemma, in normal spaces (with P always true) and in locally compact spaces (with P = IsCompact). We put also in the structure the assumption that, for any such pair, one may find an intermediate pair in between satisfying P, to avoid carrying it around in the argument.

Instances For
    theorem Urysohns.CU.P_C {X : Type u_2} [TopologicalSpace X] {P : Set XProp} (self : Urysohns.CU P) :
    P self.C
    theorem Urysohns.CU.closed_C {X : Type u_2} [TopologicalSpace X] {P : Set XProp} (self : Urysohns.CU P) :
    IsClosed self.C
    theorem Urysohns.CU.open_U {X : Type u_2} [TopologicalSpace X] {P : Set XProp} (self : Urysohns.CU P) :
    IsOpen self.U
    theorem Urysohns.CU.subset {X : Type u_2} [TopologicalSpace X] {P : Set XProp} (self : Urysohns.CU P) :
    self.C self.U
    theorem Urysohns.CU.hP {X : Type u_2} [TopologicalSpace X] {P : Set XProp} (self : Urysohns.CU P) {c : Set X} {u : Set X} :
    IsClosed cP cIsOpen uc u∃ (v : Set X), IsOpen v c v closure v u P (closure v)
    @[simp]
    theorem Urysohns.CU.left_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :
    c.left.C = c.C
    def Urysohns.CU.left {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :

    By assumption, for each c : CU P there exists an open set u such that c.C ⊆ u and closure u ⊆ c.U. c.left is the pair (c.C, u).

    Equations
    • c.left = { C := c.C, U := .choose, P_C := , closed_C := , open_U := , subset := , hP := }
    Instances For
      @[simp]
      theorem Urysohns.CU.right_U {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :
      c.right.U = c.U
      def Urysohns.CU.right {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :

      By assumption, for each c : CU P there exists an open set u such that c.C ⊆ u and closure u ⊆ c.U. c.right is the pair (closure u, c.U).

      Equations
      • c.right = { C := closure .choose, U := c.U, P_C := , closed_C := , open_U := , subset := , hP := }
      Instances For
        theorem Urysohns.CU.left_U_subset_right_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :
        c.left.U c.right.C
        theorem Urysohns.CU.left_U_subset {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :
        c.left.U c.U
        theorem Urysohns.CU.subset_right_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :
        c.C c.right.C
        noncomputable def Urysohns.CU.approx {X : Type u_1} [TopologicalSpace X] {P : Set XProp} :
        Urysohns.CU PX

        n-th approximation to a continuous function f : X → ℝ such that f = 0 on c.C and f = 1 outside of c.U.

        Equations
        Instances For
          theorem Urysohns.CU.approx_of_mem_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) {x : X} (hx : x c.C) :
          theorem Urysohns.CU.approx_of_nmem_U {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) {x : X} (hx : xc.U) :
          theorem Urysohns.CU.approx_nonneg {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) (x : X) :
          theorem Urysohns.CU.approx_le_one {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) (x : X) :
          theorem Urysohns.CU.bddAbove_range_approx {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
          theorem Urysohns.CU.approx_le_approx_of_U_sub_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} {c₁ : Urysohns.CU P} {c₂ : Urysohns.CU P} (h : c₁.U c₂.C) (n₁ : ) (n₂ : ) (x : X) :
          Urysohns.CU.approx n₂ c₂ x Urysohns.CU.approx n₁ c₁ x
          theorem Urysohns.CU.approx_mem_Icc_right_left {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) (x : X) :
          theorem Urysohns.CU.approx_le_succ {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (n : ) (x : X) :
          theorem Urysohns.CU.approx_mono {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
          Monotone fun (n : ) => Urysohns.CU.approx n c x
          noncomputable def Urysohns.CU.lim {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :

          A continuous function f : X → ℝ such that

          • 0 ≤ f x ≤ 1 for all x;
          • f equals zero on c.C and equals one outside of c.U;
          Equations
          Instances For
            theorem Urysohns.CU.tendsto_approx_atTop {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
            Filter.Tendsto (fun (n : ) => Urysohns.CU.approx n c x) Filter.atTop (nhds (c.lim x))
            theorem Urysohns.CU.lim_of_mem_C {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) (h : x c.C) :
            c.lim x = 0
            theorem Urysohns.CU.lim_of_nmem_U {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) (h : xc.U) :
            c.lim x = 1
            theorem Urysohns.CU.lim_eq_midpoint {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
            c.lim x = midpoint (c.left.lim x) (c.right.lim x)
            theorem Urysohns.CU.approx_le_lim {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) (n : ) :
            Urysohns.CU.approx n c x c.lim x
            theorem Urysohns.CU.lim_nonneg {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
            0 c.lim x
            theorem Urysohns.CU.lim_le_one {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
            c.lim x 1
            theorem Urysohns.CU.lim_mem_Icc {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) (x : X) :
            c.lim x Set.Icc 0 1
            theorem Urysohns.CU.continuous_lim {X : Type u_1} [TopologicalSpace X] {P : Set XProp} (c : Urysohns.CU P) :

            Continuity of Urysohns.CU.lim. See module docstring for a sketch of the proofs.

            theorem exists_continuous_zero_one_of_isClosed {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {s : Set X} {t : Set X} (hs : IsClosed s) (ht : IsClosed t) (hd : Disjoint s t) :
            ∃ (f : C(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_continuous_zero_one_of_isCompact {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
            ∃ (f : C(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 sets in a regular locally compact topological space X, with s compact and t closed, 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_continuous_one_zero_of_isCompact {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s : Set X} {t : Set X} (hs : IsCompact s) (ht : IsClosed t) (hd : Disjoint s t) :
            ∃ (f : C(X, )), Set.EqOn (⇑f) 1 s Set.EqOn (⇑f) 0 t HasCompactSupport f ∀ (x : X), f x Set.Icc 0 1

            Urysohn's lemma: if s and t are two disjoint sets in a regular locally compact topological space X, with s compact and t closed, then there exists a continuous compactly supported function f : X → ℝ such that

            • f equals one on s;
            • f equals zero on t;
            • 0 ≤ f x ≤ 1 for all x.
            theorem exists_continuous_one_zero_of_isCompact_of_isGδ {X : Type u_1} [TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s : Set X} {t : Set X} (hs : IsCompact s) (h's : IsGδ s) (ht : IsClosed t) (hd : Disjoint s t) :
            ∃ (f : C(X, )), s = f ⁻¹' {1} Set.EqOn (⇑f) 0 t HasCompactSupport f ∀ (x : X), f x Set.Icc 0 1

            Urysohn's lemma: if s and t are two disjoint sets in a regular locally compact topological space X, with s compact and t closed, then there exists a continuous compactly supported function f : X → ℝ such that

            • f equals one on s;
            • f equals zero on t;
            • 0 ≤ f x ≤ 1 for all x.

            Moreover, if s is Gδ, one can ensure that f ⁻¹ {1} is exactly s.

            theorem exists_tsupport_one_of_isOpen_isClosed {X : Type u_1} [TopologicalSpace X] [T2Space X] {s : Set X} {t : Set X} (hs : IsOpen s) (hscp : IsCompact (closure s)) (ht : IsClosed t) (hst : t s) :
            ∃ (f : C(X, )), tsupport f s Set.EqOn (⇑f) 1 t ∀ (x : X), f x Set.Icc 0 1

            A variation of Urysohn's lemma. In a T2Space X, for a closed set t and a relatively compact open set s such that t ⊆ s, there is a continuous function f supported in s, f x = 1 on t and 0 ≤ f x ≤ 1.