English
Tietze extension for continuous maps with a closed embedding: extend f: X→ℝ from a closed subset to Y.
Русский
Титце о непрерывном отображении: продолжение из замкнутого подмножества.
LaTeX
$$$\\exists g:\\; C(Y,\\mathbb{R}), g\\circ e = f$$$
Lean4
/-- **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`. -/
theorem exists_extension_forall_mem_of_isClosedEmbedding (f : C(X, ℝ)) {t : Set ℝ} {e : X → Y} [hs : OrdConnected t]
(hf : ∀ x, f x ∈ t) (hne : t.Nonempty) (he : IsClosedEmbedding e) : ∃ g : C(Y, ℝ), (∀ y, g y ∈ t) ∧ g ∘ e = f :=
by
have h : ℝ ≃o Ioo (-1 : ℝ) 1 := orderIsoIooNegOneOne ℝ
let F : X →ᵇ ℝ :=
{ toFun := (↑) ∘ h ∘ f
continuous_toFun := continuous_subtype_val.comp (h.continuous.comp f.continuous)
map_bounded' :=
isBounded_range_iff.1 ((isBounded_Ioo (-1 : ℝ) 1).subset <| range_subset_iff.2 fun x => (h (f x)).2) }
let t' : Set ℝ := (↑) ∘ h '' t
have ht_sub : t' ⊆ Ioo (-1 : ℝ) 1 := image_subset_iff.2 fun x _ => (h x).2
have : OrdConnected t' := by
constructor
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ z hz
lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz
change z ∈ Icc (h x) (h y) at hz
rw [← h.image_Icc] at hz
rcases hz with ⟨z, hz, rfl⟩
exact ⟨z, hs.out hx hy hz, rfl⟩
have hFt : ∀ x, F x ∈ t' := fun x => mem_image_of_mem _ (hf x)
rcases F.exists_extension_forall_mem_of_isClosedEmbedding hFt (hne.image _) he with ⟨G, hG, hGF⟩
let g : C(Y, ℝ) :=
⟨h.symm ∘ codRestrict G _ fun y => ht_sub (hG y), h.symm.continuous.comp <| G.continuous.subtype_mk _⟩
have hgG : ∀ {y a}, g y = a ↔ G y = h a := @fun y a => h.toEquiv.symm_apply_eq.trans Subtype.ext_iff
refine ⟨g, fun y => ?_, ?_⟩
· rcases hG y with ⟨a, ha, hay⟩
convert ha
exact hgG.2 hay.symm
· ext x
exact hgG.2 (congr_fun hGF _)
