Theorems · Theorem · general topology

IsCountablyCompact.image

∀ {E : Type u_2} {F : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace F] {A : Set E},
  IsCountablyCompact A → ∀ {f : E → F}, Continuous f → IsCountablyCompact (f '' A)

The continuous image of a countably compact set is countably compact.

Defined in

Mathlib.Topology.Compactness.CountablyCompact

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace