English
A variant of the previous statement expressing the same product-neighborhood behavior with auxiliary simp lemmas.
Русский
Вариант предыдущего утверждения, выражающий ту же зависимость окрестностей произведения через вспомогательные леммы упрощения.
LaTeX
$$$(hp : \forall \{x\}, px x \rightarrow \forall \{y\}, py y \rightarrow p (x, y)) \rightarrow \forallᶠ x in 𝓝ˢ s, px x \rightarrow \forallᶠ y in 𝓝ˢ t, py y \rightarrow \forallᶠ q in 𝓝ˢ (s ×ˢ t), p q$$$
Lean4
theorem prod_nhdsSet {p : X × Y → Prop} {px : X → Prop} {py : Y → Prop}
(hp : ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)) (hs : ∀ᶠ x in 𝓝ˢ s, px x) (ht : ∀ᶠ y in 𝓝ˢ t, py y) :
∀ᶠ q in 𝓝ˢ (s ×ˢ t), p q :=
nhdsSet_prod_le _ _ (mem_of_superset (prod_mem_prod hs ht) fun _ ⟨hx, hy⟩ ↦ hp hx hy)
