tendstoUniformly — Mathlib

English

If F is uniformly continuous on U × V and x ∈ U, then TendstoUniformlyOn F (F x) (nhdsWithin x U) V holds.

Русский

Если F равномерно непрерывна на U×V и x ∈ U, то TendstoUniformlyOn F (F x) (nhdsWithin x U) V выполняется.

LaTeX

$$TendstoUniformlyOn F (F x) (nhdsWithin x U) V$$

Lean4

theorem tendstoUniformly [UniformSpace α] [UniformSpace γ] {U : Set α} (hU : U ∈ 𝓝 x) {F : α → β → γ}
    (hF : UniformContinuousOn ↿F (U ×ˢ (univ : Set β))) : TendstoUniformly F (F x) (𝓝 x) := by
  simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU] using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

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