English
Composition of SpectralMaps is a SpectralMap. It takes f ∘ g with underlying continuous maps and spectral data composed accordingly.
Русский
Композиция спектральных отображений образует спектральное отображение. Она задаётся как f ∘ g с соответствующим образом составляемыми непрерывными картами и спектральными данными.
LaTeX
$$$ \text{SpectralMap}.comp(f,g) = \langle f.toContinuousMap \circ g.toContinuousMap, f.spectral'.\text{comp } g.spectral' \rangle. $$$
Lean4
/-- Composition of `SpectralMap`s as a `SpectralMap`. -/
def comp (f : SpectralMap β γ) (g : SpectralMap α β) : SpectralMap α γ :=
⟨f.toContinuousMap.comp g.toContinuousMap, f.spectral'.comp g.spectral'⟩
