Urysohn's lemma

In this file we prove Urysohn's lemma exists_continuous_zero_one_of_closed: for any two disjoint closed sets s and t in a normal topological space X 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.

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 C ⊆ U. Since X is a normal topological space, for each c : CU X 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 X) (n : ℕ) : X → ℝ by recursion on n:

• c.approx 0 is the indicator of c.Uᶜ;
• c.approx (n + 1) x = (c.left.approx n x + c.right.approx n x) / 2.

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

• c.lim x ∈ [0, 1] for all x;
• c.lim equals zero on c.C and equals one outside of c.U;
• c.lim x = (c.left.lim x + c.right.lim x) / 2.

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:

• x ∈ c.left.U; then for y in a small neighborhood of x we have y ∈ c.left.U ⊆ c.right.C (hence c.right.lim x = c.right.lim y = 0) and |c.left.lim y - c.left.lim x| ≤ (3 / 4) ^ n. Then |c.lim y - c.lim x| = |c.left.lim y - c.left.lim x| / 2 ≤ (3 / 4) ^ n / 2 < (3 / 4) ^ (n + 1).
• otherwise, x ∉ c.left.right.C; then for y in a small neighborhood of x we have y ∉ c.left.right.C ⊇ c.left.left.U (hence c.left.left.lim x = c.left.left.lim y = 1), |c.left.right.lim y - c.left.right.lim x| ≤ (3 / 4) ^ n, and |c.right.lim y - c.right.lim x| ≤ (3 / 4) ^ n. Combining these inequalities, the triangle inequality, and the recurrence formula for c.lim, we get |c.lim x - c.lim y| ≤ (3 / 4) ^ (n + 1).

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

structure Urysohns.CU (X : Type u_2) [TopologicalSpace X] : Type u_2

• C : Set X
• U : Set X
• closed_C : IsClosed s.C
• open_U : IsOpen s.U
• subset : s.C ⊆ s.U

An auxiliary type for the proof of Urysohn's lemma: a pair of a closed set C and its open neighborhood U.

instance Urysohns.instInhabitedCU {X : Type u_1} [TopologicalSpace X] : Inhabited (Urysohns.CU X)

Equations

• Urysohns.instInhabitedCU = { default := { C := ∅, U := Set.univ, closed_C := (_ : IsClosed ∅), open_U := (_ : IsOpen Set.univ), subset := (_ : ∅ ⊆ Set.univ) } }

@[simp]

theorem Urysohns.CU.left_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : (Urysohns.CU.left c).C = c.C

def Urysohns.CU.left {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : Urysohns.CU X

Due to normal_exists_closure_subset, for each c : CU X 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Urysohns.CU.right_U {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : (Urysohns.CU.right c).U = c.U

def Urysohns.CU.right {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : Urysohns.CU X

Due to normal_exists_closure_subset, for each c : CU X 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

• One or more equations did not get rendered due to their size.

theorem Urysohns.CU.left_U_subset_right_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : (Urysohns.CU.left c).U ⊆ (Urysohns.CU.right c).C

theorem Urysohns.CU.left_U_subset {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : (Urysohns.CU.left c).U ⊆ c.U

theorem Urysohns.CU.subset_right_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : c.C ⊆ (Urysohns.CU.right c).C

noncomputable def Urysohns.CU.approx {X : Type u_1} [TopologicalSpace X] [NormalSpace X] : ℕ → Urysohns.CU X → X → ℝ

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

Equations

• Urysohns.CU.approx 0 x x = Set.indicator x.Uᶜ 1 x
• Urysohns.CU.approx (Nat.succ n) x x = midpoint ℝ (Urysohns.CU.approx n (Urysohns.CU.left x) x) (Urysohns.CU.approx n (Urysohns.CU.right x) x)

theorem Urysohns.CU.approx_of_mem_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) {x : X} (hx : x ∈ c.C) : Urysohns.CU.approx n c x = 0

theorem Urysohns.CU.approx_of_nmem_U {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) {x : X} (hx : ¬x ∈ c.U) : Urysohns.CU.approx n c x = 1

theorem Urysohns.CU.approx_nonneg {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) (x : X) : 0 ≤ Urysohns.CU.approx n c x

theorem Urysohns.CU.approx_le_one {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) (x : X) : Urysohns.CU.approx n c x ≤ 1

theorem Urysohns.CU.bddAbove_range_approx {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : BddAbove (Set.range fun n => Urysohns.CU.approx n c x)

theorem Urysohns.CU.approx_le_approx_of_U_sub_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] {c₁ : Urysohns.CU X} {c₂ : Urysohns.CU X} (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] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) (x : X) : Urysohns.CU.approx n c x ∈ Set.Icc (Urysohns.CU.approx n (Urysohns.CU.right c) x) (Urysohns.CU.approx n (Urysohns.CU.left c) x)

theorem Urysohns.CU.approx_le_succ {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (n : ℕ) (x : X) : Urysohns.CU.approx n c x ≤ Urysohns.CU.approx (n + 1) c x

theorem Urysohns.CU.approx_mono {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : Monotone fun n => Urysohns.CU.approx n c x

noncomputable def Urysohns.CU.lim {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (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

• Urysohns.CU.lim c x = ⨆ (n : ℕ), Urysohns.CU.approx n c x

theorem Urysohns.CU.tendsto_approx_atTop {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : Filter.Tendsto (fun n => Urysohns.CU.approx n c x) Filter.atTop (nhds (Urysohns.CU.lim c x))

theorem Urysohns.CU.lim_of_mem_C {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) (h : x ∈ c.C) : Urysohns.CU.lim c x = 0

theorem Urysohns.CU.lim_of_nmem_U {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) (h : ¬x ∈ c.U) : Urysohns.CU.lim c x = 1

theorem Urysohns.CU.lim_eq_midpoint {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : Urysohns.CU.lim c x = midpoint ℝ (Urysohns.CU.lim (Urysohns.CU.left c) x) (Urysohns.CU.lim (Urysohns.CU.right c) x)

theorem Urysohns.CU.approx_le_lim {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) (n : ℕ) : Urysohns.CU.approx n c x ≤ Urysohns.CU.lim c x

theorem Urysohns.CU.lim_nonneg {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : 0 ≤ Urysohns.CU.lim c x

theorem Urysohns.CU.lim_le_one {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : Urysohns.CU.lim c x ≤ 1

theorem Urysohns.CU.lim_mem_Icc {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) (x : X) : Urysohns.CU.lim c x ∈ Set.Icc 0 1

theorem Urysohns.CU.continuous_lim {X : Type u_1} [TopologicalSpace X] [NormalSpace X] (c : Urysohns.CU X) : Continuous (Urysohns.CU.lim c)

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

theorem exists_continuous_zero_one_of_closed {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, 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.