fst_nhds — Mathlib

English

If f: X → Y × Z tends to p in nhds, then the first-coordinate projection of f tends to p1 in nhds.

Русский

Если f стремится к p в nhds, то первая координата x ↦ (f x)₁ сходится к p₁ в nhds.

LaTeX

$$$\\text{Tendsto } f\\ l\\ (\\mathcal{nhds} p) \\Rightarrow \\text{Tendsto } a \\mapsto (f a)_1\ l\\ (\\mathcal{nhds} p_1)$$$

Lean4

theorem fst_nhds {X} {l : Filter X} {f : X → Y × Z} {p : Y × Z} (h : Tendsto f l (𝓝 p)) :
    Tendsto (fun a ↦ (f a).1) l (𝓝 <| p.1) :=
  continuousAt_fst.tendsto.comp h

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