English
Re-statement: Under the same hypotheses as earlier, the uniform space on C(α,β) equals the infimum of the comaps by the cover maps.
Русский
Повторное высказывание: при тех же условиях униформное пространство на C(α,β) равно infimum от компап по покрытиям φ_i.
LaTeX
$$$\text{UniformSpace } C(α, β) = \inf_i (\text{comap}(·, φ_i))$$$
Lean4
/-- If the topology on `α` is generated by its restrictions to compact sets, then the space of
continuous maps `C(α, β)` is complete (w.r.t. the compact convergence uniformity).
Sufficient conditions on `α` to satisfy this condition are (weak) local compactness and sequential
compactness. -/
instance instCompleteSpaceOfCompactlyCoherentSpace [CompactlyCoherentSpace α] : CompleteSpace C(α, β) :=
by
rw [completeSpace_iff_isComplete_range isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing,
range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete]
exact (UniformOnFun.isClosed_setOf_continuous CompactlyCoherentSpace.isCoherentWith).completeSpace_coe
