English
Let f1: ι → κ and f2 i: σ_i → τ (f1 i) with h1 Injective f1. Then the induced map Sigma.map f1 f2 is inducing iff ∀ i, IsInducing (f2 i).
Русский
Пусть f1: ι → κ и отображения f2_i: σ_i → τ (f1 i) удовлетворяют условию, что f1 инъективен. Тогда индуктивное отображение Sigma.map f1 f2 является индукирующим тогда и только тогда, когда каждое отображение f2_i индуктивно.
LaTeX
$$$ (h_1 : \operatorname{Injective}(f_1)) \\Rightarrow \\mathrm{IsInducing}(\\mathrm{Sigma.map} f_1 f_2) \\Leftrightarrow \\forall i, \\mathrm{IsInducing}(f_2 i).$$$
Lean4
theorem isInducing_sigmaMap {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (h₁ : Injective f₁) :
IsInducing (Sigma.map f₁ f₂) ↔ ∀ i, IsInducing (f₂ i) := by
simp only [isInducing_iff_nhds, Sigma.forall, Sigma.nhds_mk, Sigma.map_mk, ← map_sigma_mk_comap h₁,
map_inj sigma_mk_injective]
