isSpectralMap

Mathlib.Topology.Spectral.Hom

URI: https://scilib.ai/kg/mathlib#IsProperMap.isSpectralMap

English

A proper map is a spectral map.

Русский

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

LaTeX

$$$ IsProperMap(f) \Rightarrow IsSpectralMap(f). $$$

Lean4

theorem isSpectralMap {f : α → β} (hf : IsProperMap f) : IsSpectralMap f :=
  ⟨hf.toContinuous, fun _ _ ↦ hf.isCompact_preimage⟩

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

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

Разделы

Аффилиация

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