English
The restriction of a compact closed set to a subset of coordinates is closed.
Русский
Ограничение компактно замкнутого множества к подмножеству координат остается замкнутым.
LaTeX
$$$\\text{IsClosed}(S^{\\text{re}} \\'\, s)\\; \\text{given } s \\text{ compact and closed}.$$$
Lean4
/-- The restriction of a compact closed set in a product space to a set of coordinates is closed. -/
theorem isClosed_image_restrict (S : Set ι) (hs_compact : IsCompact s) (hs_closed : IsClosed s) :
IsClosed (S.restrict '' s) := by
rw [← Topology.image_snd_preimageImageRestrict]
have : CompactSpace (Sᶜ.restrict '' s) := isCompact_iff_compactSpace.mp (hs_compact.image (Pi.continuous_restrict _))
refine isClosedMap_snd_of_compactSpace _ ?_
rw [Homeomorph.isClosed_image]
exact hs_closed.preimage continuous_subtype_val
