Theorems · Theorem · order theory

Finset.mem_dfinsupp_iff_of_support_subset

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (α i)] {s : Finset ι}
  {f : Π₀ (i : ι), α i} [inst_2 : (i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)},
  t.support ⊆ s → (f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i)

When t is supported on s, f ∈ s.dfinsupp t precisely means that f is pointwise in t.

Defined in

Mathlib.Data.DFinsupp.Interval

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqZeroDecidableEq