α : Type u_1
β : Type u_2
γ : Type ?u.2117
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ s_1 x u_1 x, CompactOpen.gen s u = CompactOpen.gen s_1 u_1
α : Type u_1
β : Type u_2
γ : Type ?u.2117
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ CompactOpen.gen s u ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
dsimp [mem_setOf_eq]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2117
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set α
hs : IsCompact s
u : Set β
hu : IsOpen u
⊢ ∃ s_1 x u_1 x, CompactOpen.gen s u = CompactOpen.gen s_1 u_1
tauto