X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.31928
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
⊢ ↑{ toFun := ↑g ∘ f, isLocallyConstant := (_ : IsLocallyConstant (g.toFun ∘ f)) } = ↑g ∘ f
X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.31928
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
⊢ ↑(comap f g) = ↑g ∘ f
rw [comap, dif_pos hf]
no goals
X : Type u_3
Y : Type u_1
Z : Type u_2
α : Type ?u.31928
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
g : LocallyConstant Y Z
hf : Continuous f
⊢ ↑{ toFun := ↑g ∘ f, isLocallyConstant := (_ : IsLocallyConstant (g.toFun ∘ f)) } = ↑g ∘ f
rfl