Theorems · Inductive type · general topology
IsSpectralMap
{α : Type u_2} → {β : Type u_3} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → PropA function between topological spaces is spectral if it is continuous and the preimage of every compact open set is compact open.
- Defined in
- Mathlib.Topology.Spectral.Hom
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by30
Results whose statement or proof uses this declaration.
- IsSpectralMap.isCompact_preimage_of_isOpenstatement and proof · cited by 5
- Function.locallyFinsupp.mapstatement and proof · cited by 4
- AlgebraicGeometry.quasiCompact_iff_isSpectralMapstatement and proof · cited by 2
- IsSpectralMap.toContinuousstatement and proof · cited by 2
- IsRetrocompact_iff_isSpectralMap_subtypeValstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.Hom.isSpectralMapstatement · cited by 2
- IsCompact.preimage_of_isOpenstatement and proof · cited by 2
- IsSpectralMap.continuousstatement and proof · cited by 1
- SpectralMap.mk.injstatement and proof · cited by 1
- SpectralMap.mk.noConfusionstatement and proof · cited by 1
- IsProperMap.isSpectralMapstatement · cited by 1
- isSpectralMap_idstatement · cited by 1