toContinuousMap — Mathlib

English

Every spectral map can be regarded as a continuous map.

Русский

Каждое спектральное отображение может рассматриваться как непрерывное отображение.

LaTeX

$$$ \forall f:\SpectralMap(\alpha,\beta),\; toContinuousMap(f) \in \text{ContinuousMap}(\alpha,\beta). $$$

Lean4

/-- Reinterpret a `SpectralMap` as a `ContinuousMap`. -/
def toContinuousMap (f : SpectralMap α β) : ContinuousMap α β :=
  ⟨_, f.spectral'.continuous⟩

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