curry_nhds — Mathlib

English

If a property p on X × Y holds eventually in nhds (x,y), then it holds eventually in nhds x for all y and nhds y for all x, when appropriately curry-transformed.

Русский

Если свойство p на X × Y выполняется почти постоянно в nhds (x,y), то оно выполняется почти постоянно в nhds x для переменного y и в nhds y для переменного x после карри-преобразования.

LaTeX

$$$ \\mathrm{nhds\\_prod\\_eq} \\Rightarrow \\text{(curry form) } \\text{(переход)}$$$

Lean4

theorem curry_nhds {p : X × Y → Prop} {x : X} {y : Y} (h : ∀ᶠ x in 𝓝 (x, y), p x) :
    ∀ᶠ x' in 𝓝 x, ∀ᶠ y' in 𝓝 y, p (x', y') := by
  rw [nhds_prod_eq] at h
  exact h.curry

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