English
A function that can be locally uniformly approximated by functions continuous within a set at a point is continuous within the set at that point.
Русский
Функция, которую можно локально равномерно аппроксимировать функциями, непрерывными внутри множества в данной точке, непрерывна внутри множества в этой точке.
LaTeX
$$$\forall x\in s,\ (\forall u\in 𝓤(\beta),\exists t\in 𝓝[s] x,\exists F,\ ContinuousWithinAt(F,s,x) \land \forall y\in t, (f(y),F(y))\in u) \Rightarrow \mathrm{ContinuousWithinAt}(f,s,x)$$$
Lean4
/-- A function which can be locally uniformly approximated by functions which are continuous
within a set at a point is continuous within this set at this point. -/
theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (hx : x ∈ s)
(L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F : α → β, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
ContinuousWithinAt f s x :=
by
refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_
obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ u ∈ 𝓤 β, (∀ {a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁ := comp_symm_of_uniformity h₁
rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩
have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF
have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂
have C : ∀ᶠ y in 𝓝[s] x, (f y, F x) ∈ u₁ := (A.and B).mono fun y hy => u₂₁ (prodMk_mem_compRel hy.1 hy.2)
have : (F x, f x) ∈ u₁ := u₂₁ (prodMk_mem_compRel (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
exact C.mono fun y hy => u₁₀ (prodMk_mem_compRel hy this)
