∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  {s : TopologicalSpace.Clopens α} {t : TopologicalSpace.Clopens β} {x : α × β}, x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t