isClosedMap_snd_of_compactSpace — Mathlib

English

If Y is compact, then the projection Prod.fst: X × Y → X is a closed map.

Русский

Если Y компактно, проекция Prod.fst: X × Y → X — замкнутое отображение.

LaTeX

$$IsClosedMap(Prod.fst)$$

Lean4

/-- If `X` is a compact topological space, then `Prod.snd : X × Y → Y` is a closed map. -/
theorem isClosedMap_snd_of_compactSpace [CompactSpace X] : IsClosedMap (Prod.snd : X × Y → Y) := fun s hs =>
  by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro y hy
  have : univ ×ˢ { y } ⊆ sᶜ := by exact fun (x, y') ⟨_, rfl⟩ hs => hy ⟨(x, y'), hs, rfl⟩
  rcases generalized_tube_lemma isCompact_univ isCompact_singleton hs.isOpen_compl this with ⟨U, V, -, hVo, hU, hV, hs⟩
  refine mem_nhds_iff.2 ⟨V, ?_, hVo, hV rfl⟩
  rintro _ hzV ⟨z, hzs, rfl⟩
  exact hs ⟨hU trivial, hzV⟩ hzs

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