α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.127862
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set α
hs : IsCompact s
ht : IsCompact t
hst : s ×ˢ t ⊆ diagonal αᶜ
⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ diagonal αᶜ
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.127862
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set α
hs : IsCompact s
ht : IsCompact t
hst : Disjoint s t
⊢ SeparatedNhds s t
simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.127862
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
s t : Set α
hs : IsCompact s
ht : IsCompact t
hst : s ×ˢ t ⊆ diagonal αᶜ
⊢ ∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ diagonal αᶜ
exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst