isClosedMap_restrict_of_compactSpace

English

If every factor space is compact, the projection restricting to a subset of coordinates is a closed map.

Русский

Если все пространства компактны, проекция, ограничивающая координаты до поднабора, является замкнутым отображением.

LaTeX

$$$\\text{IsClosedMap}(\\,S.restrict\\;): (\\Pi i, \\alpha_i) \\to (\\Pi i\\in S, \\alpha_i)\\;\\text{ при } \\forall i,\\text{CompactSpace}(\\alpha_i).$$$

Lean4

theorem isClosedMap_restrict_of_compactSpace [∀ i, CompactSpace (α i)] : IsClosedMap (S.restrict : (Π i, α i) → _) :=
  fun s hs ↦ by
  classical
  have : S.restrict (π := α) = Prod.fst ∘ (Homeomorph.piEquivPiSubtypeProd S α) := rfl
  rw [this, image_comp]
  exact isClosedMap_fst_of_compactSpace _ <| (Homeomorph.isClosed_image _).mpr hs

Похожие утверждения