Theorems · Theorem · general topology

IsClosed.isClosed_image_eval

∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} [inst : (i : ι) → TopologicalSpace (α i)] (i : ι),
  IsCompact s → IsClosed s → IsClosed ((fun x => x i) '' s)

Defined in

Mathlib.Topology.IsClosedRestrict

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpace