Theorems · Theorem · general topology

IsCompact.isClosed_image_restrict

∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [inst : (i : ι) → TopologicalSpace (α i)] (S : Set ι),
  IsCompact s → IsClosed s → IsClosed (S.domRestrict '' s)

The restriction of a compact closed set in a product space to a set of coordinates is closed.

Defined in

Mathlib.Topology.IsClosedRestrict

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace