prodMap — Mathlib

English

If f: X → Y and g: Z → W are open maps, then Prod.map f g is an open map.

Русский

Если f: X → Y и g: Z → W — открытые отображения, то Prod.map f g — открытое отображение.

LaTeX

$$$\IsOpenMap f \land \IsOpenMap g \Rightarrow \IsOpenMap(\mathrm{Prod.map} f g)$$$

Lean4

protected theorem prodMap {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Prod.map f g) :=
  by
  rw [isOpenMap_iff_nhds_le]
  rintro ⟨a, b⟩
  rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq']
  exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

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