English
For equicontinuous F on a compact X, F tends to f uniformly iff F tends to f pointwise along any filter.
Русский
Для равномерно ограниченного F на компактном X схождение к f по униформной структуре эквивалентно по точечному схождению.
LaTeX
$$$ Tendsto (UniformFun.ofFun \circ F) \mathcal{F} (\mathcal{N} (UniformFun.ofFun f)) \iff Tendsto F \mathcal{F} (\mathcal{N} f) $$$
Lean4
/-- Let `X` be a compact topological space, `α` a uniform space, `F : ι → (X → α)` an
equicontinuous family, and `ℱ` a filter on `ι`. Then, `F` tends *uniformly* to `f : X → α` along
`ℱ` iff it tends to `f` *pointwise* along `ℱ`. -/
theorem tendsto_uniformFun_iff_pi [CompactSpace X] (F_eqcont : Equicontinuous F) (ℱ : Filter ι) (f : X → α) :
Tendsto (UniformFun.ofFun ∘ F) ℱ (𝓝 <| UniformFun.ofFun f) ↔ Tendsto F ℱ (𝓝 f) := by
-- Assume `ℱ` is non-trivial.
rcases ℱ.eq_or_neBot with rfl | ℱ_ne
· simp
constructor <;> intro H
· exact UniformFun.uniformContinuous_toFun.continuous.tendsto _ |>.comp H
· set S : Set (X → α) := closure (range F)
set 𝒢 : Filter S :=
comap (↑)
(map F ℱ)
-- We would like to use `Equicontinuous.comap_uniformFun_eq`, but applying it to `F` is not
-- enough since `f` has no reason to be in the range of `F`.
-- Instead, we will apply it to the inclusion `(↑) : S → (X → α)` where `S` is the closure of
-- the range of `F` *for the product topology*.
-- We know that `S` is still equicontinuous...
have hS : S.Equicontinuous := closure' (by rwa [equicontinuous_iff_range] at F_eqcont) continuous_id
have ind : IsInducing (UniformFun.ofFun ∘ (↑) : S → X →ᵤ α) :=
hS.inducing_uniformFun_iff_pi.mpr
⟨rfl⟩
-- By construction, `f` is in `S`.
have f_mem : f ∈ S := mem_closure_of_tendsto H range_mem_map
have h𝒢ℱ : map (↑) 𝒢 = map F ℱ :=
Filter.map_comap_of_mem (Subtype.range_coe ▸ mem_of_superset range_mem_map subset_closure)
have H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩) := by rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]
rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'
