tendsto_prod_principal_iff — Mathlib

English

Uniform convergence on a product with a principal filter on a set is equivalent to standard uniform convergence on that set.

Русский

Сходимость по произведению с простым фильтром на множество эквивалентна обычной равномерной сходимости на этом множестве.

LaTeX

$$Tendsto ↿F (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun _ => c) p s$$

Lean4

/-- Uniform convergence on a set `s` to a constant function is equivalent to convergence in
`p ×ˢ 𝓟 s`. -/
theorem tendsto_prod_principal_iff {c : β} : Tendsto ↿F (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun _ => c) p s :=
  by
  rw [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter]
  exact tendsto_prod_filter_iff

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