piMap — Mathlib

English

If each f_i is an open map and surjective in a cofinite sense, then the product map Pi.map f is an open map.

Русский

Если каждый f_i открыто отображает, и на кофиний совокупности отображается сюръекция, то произведение отображений Pi.map f открыто.

LaTeX

$$$$ \mathrm{IsOpenMap}(\Pi.Map(f)) $$$$

Lean4

protected theorem piMap {f : ∀ i, A i → B i} (hfo : ∀ i, IsOpenMap (f i)) (hsurj : ∀ᶠ i in cofinite, Surjective (f i)) :
    IsOpenMap (Pi.map f) := by
  refine IsOpenMap.of_nhds_le fun x ↦ ?_
  rw [nhds_pi, nhds_pi, map_piMap_pi hsurj]
  exact Filter.pi_mono fun i ↦ (hfo i).nhds_le _

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