piMap — Mathlib

English

If each f i is an open embedding, then Pi.map f is an open embedding (for finite index set).

Русский

Если каждый компонент является открытым вложением, то произведение отображений открытo вложение.

LaTeX

$$$\\displaystyle \\text{piMap}\\bigl(\\,\\text{hf}: \\forall i, \\text{IsOpenEmbedding}(f_i)\\bigr) : \\text{IsOpenEmbedding}(\\Pi\\text{-map } f).$$$

Lean4

protected theorem piMap [Finite ι] {f : ∀ i, A i → B i} (hf : ∀ i, IsOpenEmbedding (f i)) :
    IsOpenEmbedding (Pi.map f) :=
  ⟨.piMap fun i ↦ (hf i).1, by simpa using isOpen_set_pi Set.finite_univ fun i _ ↦ (hf i).2⟩

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