α : Type u
β : Type v
γ : Type ?u.63807
δ : Type ?u.63810
ε : Type ?u.63813
ζ : Type ?u.63816
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
hs : Dense s
ht : Dense t
x : α × β
⊢ x ∈ closure s ×ˢ closure t
α : Type u
β : Type v
γ : Type ?u.63807
δ : Type ?u.63810
ε : Type ?u.63813
ζ : Type ?u.63816
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
hs : Dense s
ht : Dense t
x : α × β
⊢ x ∈ closure (s ×ˢ t)
rw [closure_prod_eq]
no goals
α : Type u
β : Type v
γ : Type ?u.63807
δ : Type ?u.63810
ε : Type ?u.63813
ζ : Type ?u.63816
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
s : Set α
t : Set β
hs : Dense s
ht : Dense t
x : α × β
⊢ x ∈ closure s ×ˢ closure t
exact ⟨hs x.1, ht x.2⟩