continuous_of_uniform_approx_of_continuous

English

The product of uniform spaces with ultra-uniformities has an ultra-uniformity.

Русский

Произведение равномерных пространств с ультра-равномерностями обладает ультра-равномерностью.

LaTeX

$$$IsUltraUniformity\big(X \times Y\big)$$$

Lean4

/-- A function which can be uniformly approximated by continuous functions is continuous. -/
theorem continuous_of_uniform_approx_of_continuous (L : ∀ u ∈ 𝓤 β, ∃ F, Continuous F ∧ ∀ y, (f y, F y) ∈ u) :
    Continuous f :=
  continuousOn_univ.mp <| continuousOn_of_uniform_approx_of_continuousOn <| by simpa [continuousOn_univ] using L

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