α : Type u_1
β : Type ?u.18691
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
α : Type u_1
β : Type ?u.18691
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
⊢ IsQuasiSeparated s
intro U V hU hU' hU'' hV hV' hV''
no goals
α : Type u_1
β : Type ?u.18691
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
ht : IsQuasiSeparated t
h : s ⊆ t
U V : Set α
hU : U ⊆ s
hU' : IsOpen U
hU'' : IsCompact U
hV : V ⊆ s
hV' : IsOpen V
hV'' : IsCompact V
⊢ IsCompact (U ∩ V)
exact ht U V (hU.trans h) hU' hU'' (hV.trans h) hV' hV''