English
Let f1: ι → κ and a family of maps f2_i: σ_i → τ (f1(i)). The induced map Sigma.map f1 f2: Σ i, σ_i → Σ i, τ (f1 i) is an open map if and only if each f2_i is an open map.
Русский
Пусть f1: ι → κ и семейство отображений f2_i: σ_i → τ (f1(i)). Индуктивное отображение Sigma.map f1 f2: Σ i, σ_i → Σ i, τ (f1(i)) является открытым отображением тогда и только тогда, когда каждое отображение f2_i является открытым отображением.
LaTeX
$$$\\mathrm{IsOpenMap}(\\mathrm{Sigma.map} f_1 f_2) \\Leftrightarrow \\forall i, \\mathrm{IsOpenMap}(f_2 i).$$$
Lean4
theorem isOpenMap_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} :
IsOpenMap (Sigma.map f₁ f₂) ↔ ∀ i, IsOpenMap (f₂ i) :=
isOpenMap_sigma.trans <| forall_congr' fun i => (@IsOpenEmbedding.sigmaMk _ _ _ (f₁ i)).isOpenMap_iff.symm
