Theorems · Theorem · general topology

Topology.IsInducing.isCompact_preimage

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → IsClosed (Set.range f) → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)

The preimage of a compact set under an inducing map is a compact set.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace