Theorems · Definition · general algebraic systems

DFinsupp.extendWith

{ι : Type u} →
  {α : Option ι → Type v} →
    [inst : (i : Option ι) → Zero (α i)] → α none → (Π₀ (i : ι), α (some i)) → Π₀ (i : Option ι), α i

Adds a term to a dfinsupp, making a dfinsupp indexed by an Option. This is the dfinsupp version of Option.rec.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

5 results in Mathlib

Foundations

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

Assumes

Zero