prodMk_nhds — Mathlib

English

If mx tends to x and my tends to y, then the map c ↦ (mx c, my c) tends to (x,y).

Русский

Если mx сходится к x и my сходится к y, то отображение c ↦ (mx c, my c) сходится к (x,y).

LaTeX

$$$ \\mathrm{Tendsto}\\; mx\\; f\\; (\\mathcal{N} x) \\land \\mathrm{Tendsto}\\; my\\; f\\; (\\mathcal{N} y) \\Rightarrow \\mathrm{Tendsto}\\ (\\\\lambda c. (mx c, my c))\\; f\\; (\\mathcal{N} (x, y)) $$$

Lean4

theorem prodMk_nhds {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y} (hx : Tendsto mx f (𝓝 x))
    (hy : Tendsto my f (𝓝 y)) : Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y)) :=
  by
  rw [nhds_prod_eq]
  exact hx.prodMk hy

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