tendsto_pi_nhds — Mathlib

English

Tendsto f u to nhds g is equivalent to ∀x, Tendsto (λ i, f i x) u to nhds (g x).

Русский

Сходимость f к g в фильтре u эквивалентна ∀x, сходимость соответствующих координат к g x.

LaTeX

$$$$ \mathrm{Tendsto}(f, u, \mathrm{nhds}(g)) \iff \forall x, \mathrm{Tendsto}(\lambda i. f(i)(x), u, \mathrm{nhds}(g(x))) $$$$

Lean4

theorem tendsto_pi_nhds {f : Y → ∀ i, A i} {g : ∀ i, A i} {u : Filter Y} :
    Tendsto f u (𝓝 g) ↔ ∀ x, Tendsto (fun i => f i x) u (𝓝 (g x)) := by rw [nhds_pi, Filter.tendsto_pi]

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