no goals
X : Type u_2
Y : Type u_1
Z : Type ?u.15556
α : Type ?u.15559
ι : Type ?u.15562
π : ι → Type ?u.15567
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
simp only [Specializes, nhds_prod_eq, prod_le_prod]