no goals
F : Type ?u.8928
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.8940
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : SpectralMap β γ
g : SpectralMap α β
⊢ ↑f ∘ ↑g = ↑(ContinuousMap.mk ↑f) ∘ ↑(ContinuousMap.mk ↑g)
rfl