# Tietze extension theorem #

In this file we prove a few version of the Tietze extension theorem. The theorem says that a
continuous function `s → ℝ`

defined on a closed set in a normal topological space `Y`

can be
extended to a continuous function on the whole space. Moreover, if all values of the original
function belong to some (finite or infinite, open or closed) interval, then the extension can be
chosen so that it takes values in the same interval. In particular, if the original function is a
bounded function, then there exists a bounded extension of the same norm.

The proof mostly follows https://ncatlab.org/nlab/show/Tietze+extension+theorem. We patch a small
gap in the proof for unbounded functions, see
`exists_extension_forall_exists_le_ge_of_isClosedEmbedding`

.

In addition we provide a class `TietzeExtension`

encoding the idea that a topological space
satisfies the Tietze extension theorem. This allows us to get a version of the Tietze extension
theorem that simultaneously applies to `ℝ`

, `ℝ × ℝ`

, `ℂ`

, `ι → ℝ`

, `ℝ≥0`

et cetera. At some point
in the future, it may be desirable to provide instead a more general approach via
*absolute retracts*, but the current implementation covers the most common use cases easily.

## Implementation notes #

We first prove the theorems for a closed embedding `e : X → Y`

of a topological space into a normal
topological space, then specialize them to the case `X = s : Set Y`

, `e = (↑)`

.

## Tags #

Tietze extension theorem, Urysohn's lemma, normal topological space

### The `TietzeExtension`

class #

A class encoding the concept that a space satisfies the Tietze extension property.

- exists_restrict_eq' : ∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : NormalSpace X] (s : Set X), IsClosed s → ∀ (f : C(↑s, Y)), ∃ (g : C(X, Y)), ContinuousMap.restrict s g = f

## Instances

**Tietze extension theorem** for `TietzeExtension`

spaces, a version for a closed set. Let
`s`

be a closed set in a normal topological space `X`

. Let `f`

be a continuous function
on `s`

with values in a `TietzeExtension`

space `Y`

. Then there exists a continuous function
`g : C(X, Y)`

such that `g.restrict s = f`

.

**Tietze extension theorem** for `TietzeExtension`

spaces. Let `e`

be a closed embedding of a
nonempty topological space `X₁`

into a normal topological space `X`

. Let `f`

be a continuous
function on `X₁`

with values in a `TietzeExtension`

space `Y`

. Then there exists a
continuous function `g : C(X, Y)`

such that `g ∘ e = f`

.

**Tietze extension theorem** for `TietzeExtension`

spaces. Let `e`

be a closed embedding of a
nonempty topological space `X₁`

into a normal topological space `X`

. Let `f`

be a continuous
function on `X₁`

with values in a `TietzeExtension`

space `Y`

. Then there exists a
continuous function `g : C(X, Y)`

such that `g ∘ e = f`

.

This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.

This theorem is not intended to be used directly because it is rare for a set alone to
satisfy `[TietzeExtension t]`

. For example, `Metric.ball`

in `ℝ`

only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.

Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
`[TietzeExtension t]`

under some hypotheses.

This theorem is not intended to be used directly because it is rare for a set alone to
satisfy `[TietzeExtension t]`

. For example, `Metric.ball`

in `ℝ`

only satisfies it when
the radius is strictly positive, so finding this as an instance will fail.

Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
`[TietzeExtension t]`

under some hypotheses.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

Any retract of a `TietzeExtension`

space is one itself.

Any homeomorphism from a `TietzeExtension`

space is one itself.

The Tietze extension theorem for `ℝ`

.

One step in the proof of the Tietze extension theorem. If `e : C(X, Y)`

is a closed embedding
of a topological space into a normal topological space and `f : X →ᵇ ℝ`

is a bounded continuous
function, then there exists a bounded continuous function `g : Y →ᵇ ℝ`

of the norm `‖g‖ ≤ ‖f‖ / 3`

such that the distance between `g ∘ e`

and `f`

is at most `(2 / 3) * ‖f‖`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If `e : C(X, Y)`

is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ`

is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ`

of the same norm such that `g ∘ e = f`

.

**Alias** of `BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding'`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and bundled composition. If `e : C(X, Y)`

is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ`

is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ`

of the same norm such that `g ∘ e = f`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and unbundled composition. If `e : C(X, Y)`

is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ`

is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ`

of the same norm such that `g ∘ e = f`

.

**Alias** of `BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
embedding and unbundled composition. If `e : C(X, Y)`

is a closed embedding of a topological space
into a normal topological space and `f : X →ᵇ ℝ`

is a bounded continuous function, then there exists
a bounded continuous function `g : Y →ᵇ ℝ`

of the same norm such that `g ∘ e = f`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. If `f`

is a bounded continuous real-valued function defined on a closed set in a normal
topological space, then it can be extended to a bounded continuous function of the same norm defined
on the whole space.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding and a bounded continuous function that takes values in a non-trivial closed interval.
See also `exists_extension_forall_mem_of_isClosedEmbedding`

for a more general statement that works
for any interval (finite or infinite, open or closed).

If `e : X → Y`

is a closed embedding and `f : X →ᵇ ℝ`

is a bounded continuous function such that
`f x ∈ [a, b]`

for all `x`

, where `a ≤ b`

, then there exists a bounded continuous function
`g : Y →ᵇ ℝ`

such that `g y ∈ [a, b]`

for all `y`

and `g ∘ e = f`

.

**Alias** of `BoundedContinuousFunction.exists_extension_forall_mem_Icc_of_isClosedEmbedding`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding and a bounded continuous function that takes values in a non-trivial closed interval.
See also `exists_extension_forall_mem_of_isClosedEmbedding`

for a more general statement that works
for any interval (finite or infinite, open or closed).

If `e : X → Y`

is a closed embedding and `f : X →ᵇ ℝ`

is a bounded continuous function such that
`f x ∈ [a, b]`

for all `x`

, where `a ≤ b`

, then there exists a bounded continuous function
`g : Y →ᵇ ℝ`

such that `g y ∈ [a, b]`

for all `y`

and `g ∘ e = f`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a bounded continuous real-valued function on `X`

. Then there
exists a bounded continuous function `g : Y →ᵇ ℝ`

such that `g ∘ e = f`

and each value `g y`

belongs
to a closed interval `[f x₁, f x₂]`

for some `x₁`

and `x₂`

.

**Alias** of `BoundedContinuousFunction.exists_extension_forall_exists_le_ge_of_isClosedEmbedding`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a bounded continuous real-valued function on `X`

. Then there
exists a bounded continuous function `g : Y →ᵇ ℝ`

such that `g ∘ e = f`

and each value `g y`

belongs
to a closed interval `[f x₁, f x₂]`

for some `x₁`

and `x₂`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a bounded continuous real-valued function on `X`

. Let `t`

be
a nonempty convex set of real numbers (we use `OrdConnected`

instead of `Convex`

to automatically
deduce this argument by typeclass search) such that `f x ∈ t`

for all `x`

. Then there exists
a bounded continuous real-valued function `g : Y →ᵇ ℝ`

such that `g y ∈ t`

for all `y`

and
`g ∘ e = f`

.

**Alias** of `BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a bounded continuous real-valued function on `X`

. Let `t`

be
a nonempty convex set of real numbers (we use `OrdConnected`

instead of `Convex`

to automatically
deduce this argument by typeclass search) such that `f x ∈ t`

for all `x`

. Then there exists
a bounded continuous real-valued function `g : Y →ᵇ ℝ`

such that `g y ∈ t`

for all `y`

and
`g ∘ e = f`

.

**Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. Let `s`

be a closed set in a normal topological space `Y`

. Let `f`

be a bounded continuous
real-valued function on `s`

. Let `t`

be a nonempty convex set of real numbers (we use
`OrdConnected`

instead of `Convex`

to automatically deduce this argument by typeclass search) such
that `f x ∈ t`

for all `x : s`

. Then there exists a bounded continuous real-valued function
`g : Y →ᵇ ℝ`

such that `g y ∈ t`

for all `y`

and `g.restrict s = f`

.

**Tietze extension theorem** for real-valued continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a continuous real-valued function on `X`

. Let `t`

be a nonempty
convex set of real numbers (we use `OrdConnected`

instead of `Convex`

to automatically deduce this
argument by typeclass search) such that `f x ∈ t`

for all `x`

. Then there exists a continuous
real-valued function `g : C(Y, ℝ)`

such that `g y ∈ t`

for all `y`

and `g ∘ e = f`

.

**Alias** of `ContinuousMap.exists_extension_forall_mem_of_isClosedEmbedding`

.

**Tietze extension theorem** for real-valued continuous maps, a version for a closed
embedding. Let `e`

be a closed embedding of a nonempty topological space `X`

into a normal
topological space `Y`

. Let `f`

be a continuous real-valued function on `X`

. Let `t`

be a nonempty
convex set of real numbers (we use `OrdConnected`

instead of `Convex`

to automatically deduce this
argument by typeclass search) such that `f x ∈ t`

for all `x`

. Then there exists a continuous
real-valued function `g : C(Y, ℝ)`

such that `g y ∈ t`

for all `y`

and `g ∘ e = f`

.

**Alias** of `ContinuousMap.exists_extension'`

.

**Tietze extension theorem** for `TietzeExtension`

spaces. Let `e`

be a closed embedding of a
nonempty topological space `X₁`

into a normal topological space `X`

. Let `f`

be a continuous
function on `X₁`

with values in a `TietzeExtension`

space `Y`

. Then there exists a
continuous function `g : C(X, Y)`

such that `g ∘ e = f`

.

This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.

**Alias** of `ContinuousMap.exists_extension'`

.

**Alias** of `ContinuousMap.exists_extension'`

.

**Tietze extension theorem** for `TietzeExtension`

spaces. Let `e`

be a closed embedding of a
nonempty topological space `X₁`

into a normal topological space `X`

. Let `f`

be a continuous
function on `X₁`

with values in a `TietzeExtension`

space `Y`

. Then there exists a
continuous function `g : C(X, Y)`

such that `g ∘ e = f`

.

This version is provided for convenience and backwards compatibility. Here the composition is phrased in terms of bare functions.

**Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
`s`

be a closed set in a normal topological space `Y`

. Let `f`

be a continuous real-valued function
on `s`

. Let `t`

be a nonempty convex set of real numbers (we use `OrdConnected`

instead of `Convex`

to automatically deduce this argument by typeclass search) such that `f x ∈ t`

for all `x : s`

. Then
there exists a continuous real-valued function `g : C(Y, ℝ)`

such that `g y ∈ t`

for all `y`

and
`g.restrict s = f`

.

**Alias** of `ContinuousMap.exists_restrict_eq`

.

**Tietze extension theorem** for `TietzeExtension`

spaces, a version for a closed set. Let
`s`

be a closed set in a normal topological space `X`

. Let `f`

be a continuous function
on `s`

with values in a `TietzeExtension`

space `Y`

. Then there exists a continuous function
`g : C(X, Y)`

such that `g.restrict s = f`

.

**Tietze extension theorem** for real-valued continuous maps.
`ℝ`

is a `TietzeExtension`

space.

## Equations

**Tietze extension theorem** for nonnegative real-valued continuous maps.
`ℝ≥0`

is a `TietzeExtension`

space.