continuous_characterSpaceToSpectrum

English

The map from the character space to the spectrum is a continuous map for each fixed x.

Русский

Для фиксированного x отображение из пространства характеров в спектр непрерывно.

LaTeX

$$$\\text{continuous_characterSpaceToSpectrum}(x) : \\mathrm{characterSpace}(\\mathbb{C}, \\mathrm{elemental}(\\mathbb{C}, x)) \\to \\mathrm{ spectrum}(\\mathbb{C}, x)$ is continuous$$

Lean4

theorem continuous_characterSpaceToSpectrum (x : A) : Continuous (characterSpaceToSpectrum x) :=
  continuous_induced_rng.2 (map_continuous <| gelfandTransform ℂ (elemental ℂ x) ⟨x, self_mem ℂ x⟩)

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