piMap — Mathlib

English

If each component f i is a closed embedding, then Pi.map f is a closed embedding.

Русский

Если каждый компонент f i является замкнутым вложением, то Pi.map f — замкнутое вложение.

LaTeX

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

Lean4

protected theorem piMap {f : ∀ i, A i → B i} (hf : ∀ i, IsClosedEmbedding (f i)) : IsClosedEmbedding (Pi.map f) :=
  ⟨.piMap fun i ↦ (hf i).1, by simpa using isClosed_set_pi fun i _ ↦ (hf i).2⟩

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