Theorems · Theorem · general algebraic systems

DFinsupp.support_mapRange

∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β₁ i)]
  [inst_2 : (i : ι) → Zero (β₂ i)] [inst_3 : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)] {f : (i : ι) → β₁ i → β₂ i} {hf : ∀ (i : ι), f i 0 = 0}
  {g : Π₀ (i : ι), β₁ i}, (DFinsupp.mapRange f hf g).support ⊆ g.support

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroZeroDecidableDecidable