α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen s (↑g ⁻¹' u))
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (comp g ⁻¹' m)
rw [hm, preimage_gen g hs hu]
no goals
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
m : Set C(α, γ)
x✝ : m ∈ {m | ∃ s x u x, m = CompactOpen.gen s u}
s : Set α
hs : IsCompact s
u : Set γ
hu : IsOpen u
hm : m = CompactOpen.gen s u
⊢ IsOpen (CompactOpen.gen s (↑g ⁻¹' u))
exact ContinuousMap.isOpen_gen hs (hu.preimage g.2)