English
On a subset s, locally uniform convergence is equivalent to the statement with the restricted F and f on s.
Русский
На подмножестве s локальная равномерная сходимость эквивалентна утверждению для ограниченных функций.
LaTeX
$$$$\operatorname{TendstoLocallyUniformlyOn}(F,f,p,s) \iff \operatorname{TendstoLocallyUniformlyOn}(F|_{s}, f|_{s}, p, s).$$$$
Lean4
/-- On a compact space, locally uniform convergence is just uniform convergence. -/
theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace [CompactSpace α] :
TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p :=
by
refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
choose U hU using h V hV
obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
replace hU := fun x : t => (hU x).2
rw [← eventually_all] at hU
refine hU.mono fun i hi x => ?_
specialize ht (mem_univ x)
simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht
obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht
exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃
