X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.4420
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))
X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.4420
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (g ∘ f ⁻¹' s)
rw [Set.preimage_comp]
no goals
X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.4420
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous f
s : Set Z
⊢ IsOpen (f ⁻¹' (g ⁻¹' s))
exact hf.isOpen_preimage _ (hg _)