Theorems · Theorem · general topology

IsSpectralMap.isCompact_preimage_of_isOpen

∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsSpectralMap f → ∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)

A 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

5 results in Mathlib

Foundations

Depth 50 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace