no goals
α : Type u
β : Type v
γ : Type ?u.534439
δ : Type ?u.534442
ε : Type ?u.534445
ζ : Type ?u.534448
ι : 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₁
⊢ _root_.Embedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), _root_.Embedding (f₂ i)
simp only [embedding_iff, Injective.sigma_map, inducing_sigma_map h, forall_and, h.sigma_map_iff]