exists_restrict_eq — Mathlib

English

If Y is a nonempty subsingleton space, then Y admits a Tietze extension structure.

Русский

Если Y ненулевое единичное пространство, то у Y есть структура TietzeExtension.

LaTeX

$$[\\text{TietzeExtension}(Y)]$$

Lean4

/-- **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`. -/
theorem exists_restrict_eq (hs : IsClosed s) (f : C(s, Y)) : ∃ (g : C(X, Y)), g.restrict s = f :=
  TietzeExtension.exists_restrict_eq' s hs f

Похожие утверждения