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