English
A family F of maps in C(X,Y) converges in the compact-open topology if and only if for every compact s ⊆ X there exists a limit f on s such that (F_i)|_s → f in the compact-open topology on C(s,Y).
Русский
Сходится в компактно-открытой топологии тогда и только тогда, когда для каждого компактного s ⊆ X найдётся предел f на s такой, что (F_i)|_s → f в топологии на C(s,Y).
LaTeX
$$$\exists f,\text{ Tendsto } F\ l\ (\mathcal{N} f) \iff \forall s, IsCompact(s) \to \exists f, \text{ Tendsto } (i \mapsto (F i)\restriction s) l (\mathcal{N} f)$$$
Lean4
/-- A family `F` of functions in `C(X, Y)` converges in the compact-open topology, if and only if
it converges in the compact-open topology on each compact subset of `X`. -/
theorem exists_tendsto_compactOpen_iff_forall [WeaklyLocallyCompactSpace X] [T2Space Y] {ι : Type*} {l : Filter ι}
[Filter.NeBot l] (F : ι → C(X, Y)) :
(∃ f, Filter.Tendsto F l (𝓝 f)) ↔
∀ s : Set X, IsCompact s → ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f) :=
by
constructor
· rintro ⟨f, hf⟩ s _
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
· intro h
choose f hf using h
have h :
∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ :=
by
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
haveI := isCompact_iff_compactSpace.mp hs₁
haveI := isCompact_iff_compactSpace.mp hs₂
have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
exact tendsto_nhds_unique h₁ h₂
refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
rw [tendsto_compactOpen_iff_forall]
intro s hs
rw [liftCover_restrict']
exact hf s hs
