prodMap_nhds — Mathlib

English

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

Русский

Если f1 ≤ᶠ[𝓝 x] f2 и g1 ≤ᶠ[𝓝 y] g2, то Prod.map f1 g1 ≤ᶠ[𝓝 (x,y)] Prod.map f2 g2.

LaTeX

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

Lean4

theorem prodMap_nhds {α β : Type*} [LE α] [LE β] {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

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