support_mapRange_of_injective — Mathlib

English

If e: M → N satisfies e(0)=0 and isInjective, then mapRange e is injective on Finsupp α M.

Русский

Если e: M → N удовлетворяет e(0)=0 и инъективен, то mapRange e инъективна на Finsupp α M.

LaTeX

$$Injective e → Injective (mapRange e hf)$$

Lean4

theorem support_mapRange_of_injective {e : M → N} (he0 : e 0 = 0) (f : ι →₀ M) (he : Function.Injective e) :
    (Finsupp.mapRange e he0 f).support = f.support := by
  ext
  simp only [Finsupp.mem_support_iff, Ne, Finsupp.mapRange_apply]
  exact he.ne_iff' he0

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