Product of closed embeddings

Stream: Is there code for X?

[Anatole Dedecker]

Do we really not have this????

import Mathlib.Topology.Constructions

example {X Y A B : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [TopologicalSpace A] [TopologicalSpace B] (f : A → X) (g : B → Y)
    (hf : ClosedEmbedding f) (hg : ClosedEmbedding g) :
    ClosedEmbedding (Prod.map f g) := by
  refine ⟨hf.toEmbedding.prod_map hg.toEmbedding, ?_⟩
  rw [Set.range_prod_map]
  exact hf.isClosed_range.prod hg.isClosed_range

[Yury G. Kudryashov]

We also don't have a similar statement about closed maps.

[Anatole Dedecker]

Oh I missed your message. The reason we don't have the closed map version is that it is not true without some properness assumption, see docs#isProperMap_iff_universally_closed