continuousAt_of_locally_uniform_approx_of_continuousAt

English

A function can be locally uniformly approximated by continuousWithinAt functions on a set; hence continuousWithinAt on that set.

Русский

Функцию можно локально равномерно аппроксимировать функциями, непрерывными внутри множества; значит, она непрерывна внутри множества.

LaTeX

$$$IsUltraUniformity\text{(variant)}$$$

Lean4

/-- A function which can be locally uniformly approximated by functions which are continuous at
a point is continuous at this point. -/
theorem continuousAt_of_locally_uniform_approx_of_continuousAt
    (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ F, ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousAt f x :=
  by
  rw [← continuousWithinAt_univ]
  apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _
  simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

Похожие утверждения