map_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_injective : Function.Injective (map f) ↔ ∀ i, Function.Injective (f i) := by
  classical exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

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