# 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

`f`

equals zero on`s`

;`f`

equals one on`t`

;`0 ≤ f x ≤ 1`

for all`x`

.

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
`C ⊆ U`

. 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`

:

`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, locally compact topological space

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 inbetween satisfying `P`

, to avoid carrying it around in the argument.

- C : Set X
The inner set in the inductive construction towards Urysohn's lemma

- U : Set X
The outer set in the inductive construction towards Urysohn's lemma

- P_C : P self.C
- closed_C : IsClosed self.C
- open_U : IsOpen self.U
- subset : self.C ⊆ self.U

## Instances For

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

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

## Instances For

`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 = x✝.Uᶜ.indicator 1 x
- Urysohns.CU.approx n.succ x✝ x = midpoint ℝ (Urysohns.CU.approx n x✝.left x) (Urysohns.CU.approx n x✝.right x)

## Instances For

A continuous function `f : X → ℝ`

such that

## Equations

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

## Instances For

Continuity of `Urysohns.CU.lim`

. See module docstring for a sketch of the proofs.

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`

.

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`

.

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`

.

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`

.