no goals
α : Type u
β : Type v
ι : Type ?u.56931
π : ι → Type ?u.56936
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x : α
y : β
n : Set (α × β)
hn : IsOpen n
hp : {x} ×ˢ {y} ⊆ n
⊢ (x, y) ∈ {x} ×ˢ {y}
simp
no goals
α : Type u
β : Type v
ι : Type ?u.56931
π : ι → Type ?u.56936
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x : α
y : β
n : Set (α × β)
hn : IsOpen n
hp : {x} ×ˢ {y} ⊆ n
u : Set α
v : Set β
uo : IsOpen u
vo : IsOpen v
xu : x ∈ u
yv : y ∈ v
hp' : u ×ˢ v ⊆ n
⊢ {x} ⊆ u
simpa
no goals
α : Type u
β : Type v
ι : Type ?u.56931
π : ι → Type ?u.56936
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
x : α
y : β
n : Set (α × β)
hn : IsOpen n
hp : {x} ×ˢ {y} ⊆ n
u : Set α
v : Set β
uo : IsOpen u
vo : IsOpen v
xu : x ∈ u
yv : y ∈ v
hp' : u ×ˢ v ⊆ n
⊢ {y} ⊆ v
simpa