tendstoLocallyUniformly_iff_forall_tendsto

English

TendstoLocallyUniformly F f p on α is equivalent to requiring that for every x in α, Tendsto of the pair (f, F) on p × nhds x to the uniformity on β.

Русский

Сходимость локально-равномерная для всей области эквивалентна требованию, чтобы в каждой точке x выполнялось предельное поведение пары (f, F) на p × nhds x в отношении униформности β.

LaTeX

$$$$\operatorname{TendstoLocallyUniformly} (F,f,p) \iff \forall x,\ \operatorname{Tendsto}\bigl((i,y) \mapsto (f(y), F(i,y))\bigr)\bigl(p \times\mathcal{N}_{\mathsf{a}}(x)\bigr) \bigl(\mathcal{U}(\beta)\bigr).$$$$

Lean4

theorem tendstoLocallyUniformly_iff_forall_tendsto :
    TendstoLocallyUniformly F f p ↔ ∀ x, Tendsto (fun y : ι × α => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) := by
  simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

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