continuousOn_of_locally_uniform_approx_of_continuousWithinAt

English

If a function can be locally uniformly approximated by functions continuous on a set, then it is continuous on that set.

Русский

Если функцию можно локально равномерно аппроксимировать функциями, непрерывными на множестве, то она непрерывна на этом множестве.

LaTeX

$$$\forall s, \text{ContinuousOn}(f,s) \text{ if } \exists L$$$

Lean4

/-- A function which can be locally uniformly approximated by functions which are continuous
on a set is continuous on this set. -/
theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt
    (L : ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) :
    ContinuousOn f s := fun x hx => continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt hx (L x hx)

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