continuous

Mathlib.Topology.Spectral.Hom

URI: https://scilib.ai/kg/mathlib#IsSpectralMap.continuous

English

If f is a spectral map, then f is continuous.

Русский

Если f — спектральное отображение, то оно непрерывно.

LaTeX

$$$\text{IsSpectralMap}(f) \Rightarrow \text{Continuous}(f)$$$

Lean4

theorem continuous {f : α → β} (hf : IsSpectralMap f) : Continuous f :=
  hf.toContinuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru