prodMap_nhds — Mathlib

English

If f1 =ᶠ[𝓝 x] f2 and g1 =ᶠ[𝓝 y] g2, then Prod.map f1 g1 =ᶠ[𝓝 (x,y)] Prod.map f2 g2.

Русский

Если f1 эквивалентно f2 вплоть до 𝓝 x и g1 эквивалентно g2 вплоть до 𝓝 y, то применив Prod.map получим эквивалентность вдоль 𝓝 (x,y).

LaTeX

$$$ (f_1 =\\!\\!\\!\\[𝓝 x\\] f_2) \\land (g_1 =\\!\\!\\!\\[𝓝 y\\] g_2) \\Rightarrow Prod.map\\ f_1\\ g_1 =\\!\\!\\!\\[𝓝 (x, y)\\] Prod.map\\ f_2\\ g_2 $$$

Lean4

theorem prodMap_nhds {α β : Type*} {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ =ᶠ[𝓝 x] f₂)
    (hg : g₁ =ᶠ[𝓝 y] g₂) : Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂ :=
  by
  rw [nhds_prod_eq]
  exact hf.prodMap hg

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