piMap — Mathlib

English

If each f_i is an open quotient map, then Pi.map f is an open quotient map.

Русский

Если каждый f_i является открытым факторным отображением, то Pi.map f — открытое факторное отображение.

LaTeX

$$$$ \mathrm{IsOpenQuotientMap}(\Pi.map f) $$$$

Lean4

protected theorem piMap {f : ∀ i, A i → B i} (hf : ∀ i, IsOpenQuotientMap (f i)) : IsOpenQuotientMap (Pi.map f) :=
  ⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2, .piMap (fun i ↦ (hf i).3) <| .of_forall fun i ↦ (hf i).1⟩

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