α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : 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 (↑f '' s) u)
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : 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 ((fun g => comp g f) ⁻¹' m)
rw [hm, image_gen f hs hu]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : 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 (↑f '' s) u)
exact ContinuousMap.isOpen_gen (hs.image f.2) hu