no goals
α : Type u
β : Type v
γ : Type ?u.553929
δ : Type ?u.553932
ε : Type ?u.553935
ζ : Type ?u.553938
ι : Type u_1
κ : Type u_2
σ : ι → Type u_3
τ : κ → Type u_4
inst✝² : (i : ι) → TopologicalSpace (σ i)
inst✝¹ : (k : κ) → TopologicalSpace (τ k)
inst✝ : TopologicalSpace α
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
h : Injective f₁
⊢ OpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), OpenEmbedding (f₂ i)
simp only [openEmbedding_iff_embedding_open, isOpenMap_sigma_map, embedding_sigma_map h,
  forall_and]