English
Let f1: α1 → α2 be surjective and for every a: α1 the map f2 a: β1 a → β2 (f1 a) be surjective. Then Sigma.map f1 f2 is surjective.
Русский
Пусть f1: α1 → α2 сюръективен, и для каждого a: α1 отображение f2 a: β1 a → β2 (f1 a) сюръективно. Тогда Sigma.map f1 f2 сюръективно.
LaTeX
$$$\\operatorname{Surjective}(\\Sigma\\text{map } f_1 f_2) \\leftarrow\\rightarrow \\left( \\operatorname{Surjective} f_1 \\right) \\rightarrow \\left( \\forall a, \\operatorname{Surjective}(f_2 a) \\right).$$$
Lean4
theorem sigma_map {f₁ : α₁ → α₂} {f₂ : ∀ a, β₁ a → β₂ (f₁ a)} (h₁ : Surjective f₁) (h₂ : ∀ a, Surjective (f₂ a)) :
Surjective (Sigma.map f₁ f₂) := by
simp only [Surjective, Sigma.forall, h₁.forall]
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩
