Theorems · Definition · general algebraic systems

DFinsupp.filter

{ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) → Π₀ (i : ι), β i

Filter p f is the function which is f i if p i is true and 0 otherwise.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

24 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

ZeroDecidablePred