isOpenEmbedding_sigmaMap — Mathlib

English

With h injective, IsOpenEmbedding (Sigma.map f1 f2) iff ∀ i, IsOpenEmbedding (f2 i).

Русский

При условии, что f1 инъективен, IsOpenEmbedding (Sigma.map f1 f2) эквивалентно тому, что каждый f2_i является открытым вложением.

LaTeX

$$$ (h : \operatorname{Injective}(f_1)) \\Rightarrow \\mathrm{IsOpenEmbedding}(\\mathrm{Sigma.map} f_1 f_2) \\Leftrightarrow \\forall i, \\mathrm{IsOpenEmbedding}(f_2 i).$$$

Lean4

theorem isOpenEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h : Injective f₁) :
    IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsOpenEmbedding (f₂ i) := by
  simp only [isOpenEmbedding_iff_isEmbedding_isOpenMap, isOpenMap_sigma_map, isEmbedding_sigmaMap h, forall_and]

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