English
Let f1: ι → κ and f2 i: σ_i → τ (f1 i) with h injective. Then IsEmbedding (Sigma.map f1 f2) iff ∀ i, IsEmbedding (f2 i).
Русский
Пусть f1: ι → κ и отображения f2_i: σ_i → τ (f1 i) таковы, что f1 инъективен. Тогда вложение Sigma.map f1 f2 эквивалентно тому, что для каждого i отображение f2_i является вложением.
LaTeX
$$$ (h : \operatorname{Injective}(f_1)) \\Rightarrow \mathrm{IsEmbedding}(\\mathrm{Sigma.map} f_1 f_2) \\Leftrightarrow \\forall i, \\mathrm{IsEmbedding}(f_2 i).$$$
Lean4
theorem isEmbedding_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h : Injective f₁) :
IsEmbedding (Sigma.map f₁ f₂) ↔ ∀ i, IsEmbedding (f₂ i) := by
simp only [isEmbedding_iff, isInducing_sigmaMap h, forall_and, h.sigma_map_iff]
