English
If α is compactly coherent and β is a complete metric space, then C(α,β) is a complete space under the compact-convergence uniformity.
Русский
Если α компактно-однообразно связно, а β — полное пространство, то C(α,β) полно в рамках компактной конвергенции униформности.
LaTeX
$$$[CompactlyCoherentSpace α] \Rightarrow (\text{CompleteSpace } C(α, β))$ за условием, что β полно$$
Lean4
/-- If `C(α, β)` is a complete space, then for any (possibly, discontinuous) function `f`
and any set `s`, the set of functions `g : C(α, β)` that are equal to `f` on `s`
is a complete set.
Note that this set does not have to be a closed set when `β` is not T0.
This lemma is useful to prove that, e.g., the space of paths between two points
and the space of homotopies between two continuous maps are complete spaces,
without assuming that the codomain is a Hausdorff space. -/
theorem isComplete_setOf_eqOn [CompleteSpace C(α, β)] (f : α → β) (s : Set α) : IsComplete {g : C(α, β) | EqOn g f s} :=
by
classical
intro l hlc hlf
rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
have := hlc.1
have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦
by
refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
exact fun _ h ↦ (h hx).symm
have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
set g : C(α, β) := ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
