English
If f1 is injective and for every a the map f2 a is injective, then the Sigma-map Sigma.map f1 f2 is injective.
Русский
Пусть f1: α1 → α2 инъективен, и для каждого a: α1 отображение f2 a : β1 a → β2 (f1 a) инъективно. Тогда отображение Σ-map f1 f2 инъективно.
LaTeX
$$$\\operatorname{Injective}(\\Sigma\\text{map } f_1 f_2) \\rightarrow \\left( \\operatorname{Injective} f_1 \\right) \\rightarrow \\left( \\forall a, \\operatorname{Injective}(f_2 a) \\right) \\rightarrow \\operatorname{Injective}(\\Sigma\\text{map } f_1 f_2).$$$
Lean4
theorem sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Injective f₁) (h₂ : ∀ a, Injective (f₂ a)) :
Injective (Sigma.map f₁ f₂)
| ⟨i, x⟩, ⟨j, y⟩, h => by
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
obtain rfl : x = y := h₂ i (sigma_mk_injective h)
rfl
