prod_nhds — Mathlib

English

If p holds eventually in nhds x and q holds eventually in nhds y, then p and q hold eventually in nhds (x,y).

Русский

Если p выполняется практически постоянно в nhds x и q в nhds y, то p и q выполняются почти постоянно в nhds (x,y).

LaTeX

$$$ \\forall {p q}, ( \\forallᶠ x in 𝓝 x, p x) \\rightarrow ( \\forallᶠ y in 𝓝 y, q y) \\rightarrow \\forallᶠ z in 𝓝 (x, y), p z.1 \\land q z.2 $$$

Lean4

theorem prod_nhds {p : X → Prop} {q : Y → Prop} {x : X} {y : Y} (hx : ∀ᶠ x in 𝓝 x, p x) (hy : ∀ᶠ y in 𝓝 y, q y) :
    ∀ᶠ z : X × Y in 𝓝 (x, y), p z.1 ∧ q z.2 :=
  prod_mem_nhds hx hy

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