English
Existence of a bounded continuous extension with unbundled composition for a closed embedding.
Русский
Существование ограниченно непрерывного продолжения с разбитым отображением композиции для замкнутого вложения.
LaTeX
$$$\\exists g:\\ Y \\to \\mathbb{R},\\; \\|g\\| = \\|f\\| \\land g \\circ e = f$$$
Lean4
/-- 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‖`. -/
theorem tietze_extension_step (f : X →ᵇ ℝ) (e : C(X, Y)) (he : IsClosedEmbedding e) :
∃ g : Y →ᵇ ℝ, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖ :=
by
have h3 : (0 : ℝ) < 3 := by norm_num1
have h23 : 0 < (2 / 3 : ℝ) := by
norm_num1
-- In the trivial case `f = 0`, we take `g = 0`
rcases eq_or_ne f 0 with (rfl | hf)
· simp
replace hf : 0 < ‖f‖ := norm_pos_iff.2 hf
have hf3 : -‖f‖ / 3 < ‖f‖ / 3 := (div_lt_div_iff_of_pos_right h3).2 (Left.neg_lt_self hf)
have hc₁ : IsClosed (e '' (f ⁻¹' Iic (-‖f‖ / 3))) := he.isClosedMap _ (isClosed_Iic.preimage f.continuous)
have hc₂ : IsClosed (e '' (f ⁻¹' Ici (‖f‖ / 3))) := he.isClosedMap _ (isClosed_Ici.preimage f.continuous)
have hd : Disjoint (e '' (f ⁻¹' Iic (-‖f‖ / 3))) (e '' (f ⁻¹' Ici (‖f‖ / 3))) :=
by
refine disjoint_image_of_injective he.injective (Disjoint.preimage _ ?_)
rwa [Iic_disjoint_Ici, not_le]
rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩
refine ⟨g, ?_, ?_⟩
· refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_
simpa [abs_le, neg_div] using hgf y
· refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_
have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
rcases le_total (f x) (-‖f‖ / 3) with hle₁ | hle₁
·
calc
|g (e x) - f x| = -‖f‖ / 3 - f x := by
rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply, abs_of_nonneg (sub_nonneg.2 hle₁)]
_ ≤ 2 / 3 * ‖f‖ := by linarith
· rcases le_total (f x) (‖f‖ / 3) with hle₂ | hle₂
· simp only [neg_div] at *
calc
dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
_ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
_ = 2 / 3 * ‖f‖ := by linarith
·
calc
|g (e x) - f x| = f x - ‖f‖ / 3 := by
rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply, abs_of_nonneg (sub_nonneg.2 hle₂)]
_ ≤ 2 / 3 * ‖f‖ := by linarith
