map_surjective — Mathlib

English

The map on a direct sum is surjective iff each component map is surjective.

Русский

Гомоморфизм DirectSum является сюръективным тогда и только тогда, когда каждому f_i соответствует сюръективное отображение.

LaTeX

$$$$\\mathrm{map\\; } f\\text{ surjective} \\iff \\forall i,\\ \\mathrm{Surjective}(f_i).$$$$

Lean4

theorem map_surjective : Function.Surjective (map f) ↔ (∀ i, Function.Surjective (f i)) := by
  classical exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Похожие утверждения