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