English
If F is equicontinuous at x and f tends to z along nhdsWithin x S, and for all y in S the convergence holds, then F(y) tends to z along l for y = x.
Русский
Если F эконтинуален в x, f сходится к z вдоль nhdsWithin x S, и для всех y в S верна сходимость, тогда F(·, x) сходится к z вдоль l.
LaTeX
$$как выше, повторение формулировки$$
Lean4
/-- If `F : ι → X → α` is a family of functions equicontinuous at `x`,
it tends to `f y` along a filter `l` for any `y ∈ s`,
the limit function `f` tends to `z` along `𝓝[s] x`, and `x ∈ closure s`,
then `(F · x)` tends to `z` along `l`.
In some sense, this is a converse of `EquicontinuousAt.closure`. -/
theorem tendsto_of_mem_closure {l : Filter ι} {F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α}
(hF : EquicontinuousAt F x) (hf : Tendsto f (𝓝[s] x) (𝓝 z)) (hs : ∀ y ∈ s, Tendsto (F · y) l (𝓝 (f y)))
(hx : x ∈ closure s) : Tendsto (F · x) l (𝓝 z) :=
by
rw [(nhds_basis_uniformity (𝓤 α).basis_sets).tendsto_right_iff] at hf ⊢
intro U hU
rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVs, hVU⟩
rw [mem_closure_iff_nhdsWithin_neBot] at hx
have : ∀ᶠ y in 𝓝[s] x, y ∈ s ∧ (∀ i, (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V :=
eventually_mem_nhdsWithin.and <| ((hF V hV).filter_mono nhdsWithin_le_nhds).and (hf V hV)
rcases this.exists with ⟨y, hys, hFy, hfy⟩
filter_upwards [hs y hys (ball_mem_nhds _ hV)] with i hi
exact hVU ⟨_, ⟨_, hFy i, (mem_ball_symmetry hVs).2 hi⟩, hfy⟩
