toContinuousMapClass — Mathlib

English

A spectral map induces a continuous map; there is a natural way to view a spectral map as a continuous map.

Русский

Спектральное отображение задаёт непрерывное отображение; существует естественный переход спектрального отображения к непрерывному отображению.

LaTeX

$$$ [SpectralMap\ Class\ F\alpha\beta]\Rightarrow [ContinuousMapClass\ F\alpha\beta]. $$$

Lean4

instance (priority := 100) toContinuousMapClass [TopologicalSpace α] [TopologicalSpace β] [FunLike F α β]
    [SpectralMapClass F α β] : ContinuousMapClass F α β :=
  { ‹SpectralMapClass F α β› with map_continuous := fun f => (map_spectral f).continuous }

Похожие утверждения