lmap_injective — Mathlib

English

The map lmap f is injective if and only if each f_i is injective.

Русский

Отображение lmap f инъективно тогда и только тогда, когда каждое f_i инъективно.

LaTeX

$$$\\mathrm{Injective}(\\mathrm{lmap}\\ f) \\iff \\forall i, \\ \\mathrm{Injective}(f_i).$$$

Lean4

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

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