Theorems · Theorem · general algebraic systems

DFinsupp.mapRange_injective

∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0),
  Function.Injective (DFinsupp.mapRange f hf) ↔ ∀ (i : ι), Function.Injective (f i)

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

3 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ZeroZero