English
In a prespectral space, the opens of the form compact opens yield a basis for the topology.
Русский
В prespectral-пространстве базис топологии задают компактные открытые.
LaTeX
$$$[\\mathrm{PrespectralSpace}(X)] \\Rightarrow \\mathrm{Opens.IsBasis}(\\{U:\\ Opens X \\mid IsCompact(U)\\})$$$
Lean4
/-- **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`. -/
theorem exists_extension_forall_mem_Icc_of_isClosedEmbedding (f : X →ᵇ ℝ) {a b : ℝ} {e : X → Y}
(hf : ∀ x, f x ∈ Icc a b) (hle : a ≤ b) (he : IsClosedEmbedding e) :
∃ g : Y →ᵇ ℝ, (∀ y, g y ∈ Icc a b) ∧ g ∘ e = f :=
by
rcases exists_extension_norm_eq_of_isClosedEmbedding (f - const X ((a + b) / 2)) he with ⟨g, hgf, hge⟩
refine ⟨const Y ((a + b) / 2) + g, fun y => ?_, ?_⟩
· suffices ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2 by
simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using (norm_coe_le_norm g y).trans (hgf.trans_le this)
refine (norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun x => ?_
simpa only [Real.Icc_eq_closedBall] using hf x
· ext x
have : g (e x) = f x - (a + b) / 2 := congr_fun hge x
simp [this]
