English
If p holds whenever x ∈ s and y ∈ t and px(x) and py(y) imply p(x,y), and px, py hold eventually near s and t respectively, then p holds eventually on s ×ˢ t.
Русский
Если p выполняется для всех x∈s и y∈t при условии px(x) и py(y) и px, py выполняются почти где-то ближе к s и t, то p выполняется почти в s ×ˢ t.
LaTeX
$$$(hp : \forall \{x\}, px x \rightarrow \forall \{y\}, py y \rightarrow p (x, y)) \\Rightarrow (hs : \forallᶠ x in 𝓝ˢ s, px x) \\Rightarrow (ht : \forallᶠ y in 𝓝ˢ t, py y) \\Rightarrow \forallᶠ q in 𝓝ˢ (s ×ˢ t), p q$$$
Lean4
theorem eventually_nhdsSet_prod_iff {p : X × Y → Prop} :
(∀ᶠ q in 𝓝ˢ (s ×ˢ t), p q) ↔
∀ x ∈ s,
∀ y ∈ t,
∃ px : X → Prop,
(∀ᶠ x' in 𝓝 x, px x') ∧
∃ py : Y → Prop, (∀ᶠ y' in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y) :=
by simp_rw [eventually_nhdsSet_iff_forall, forall_prod_set, nhds_prod_eq, eventually_prod_iff]
