α : Type u
β : Type v
γ : Type ?u.40439
δ : Type ?u.40442
ε : Type ?u.40445
ζ : Type ?u.40448
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
p : α × β → Prop
x : α
y : β
h : ∀ᶠ (x : α × β) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y')
α : Type u
β : Type v
γ : Type ?u.40439
δ : Type ?u.40442
ε : Type ?u.40445
ζ : Type ?u.40448
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
p : α × β → Prop
x : α
y : β
h : ∀ᶠ (x : α × β) in 𝓝 (x, y), p x
⊢ ∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y')
rw [nhds_prod_eq] at h
no goals
α : Type u
β : Type v
γ : Type ?u.40439
δ : Type ?u.40442
ε : Type ?u.40445
ζ : Type ?u.40448
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
p : α × β → Prop
x : α
y : β
h : ∀ᶠ (x : α × β) in 𝓝 x ×ˢ 𝓝 y, p x
⊢ ∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y')
exact h.curry