case h.mk
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ mk g ∈ (fun g => comp g f) ⁻¹' CompactOpen.gen s u ↔ mk g ∈ CompactOpen.gen (↑f '' s) u
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
⊢ (fun g => comp g f) ⁻¹' CompactOpen.gen s u = CompactOpen.gen (↑f '' s) u
ext ⟨g, _⟩
case h.mk
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ g ∘ ↑f '' s ⊆ u ↔ g '' (↑f '' s) ⊆ u
case h.mk
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ mk g ∈ (fun g => comp g f) ⁻¹' CompactOpen.gen s u ↔ mk g ∈ CompactOpen.gen (↑f '' s) u
change g ∘ f '' s ⊆ u ↔ g '' (f '' s) ⊆ u
no goals
case h.mk
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g✝ : C(β, γ)
f : C(α, β)
s : Set α
x✝¹ : IsCompact s
u : Set γ
x✝ : IsOpen u
g : β → γ
continuous_toFun✝ : Continuous g
⊢ g ∘ ↑f '' s ⊆ u ↔ g '' (↑f '' s) ⊆ u
rw [Set.image_comp]