Theorems · Definition · order theory

Finsupp.rangeIcc

{ι : Type u_1} →
  {α : Type u_2} →
    [inst : Zero α] →
      [inst_1 : PartialOrder α] → [LocallyFiniteOrder α] → [DecidableEq ι] → (ι →₀ α) → (ι →₀ α) → ι →₀ Finset α

Pointwise Finset.Icc bundled as a Finsupp.

Defined in

Mathlib.Data.Finsupp.Interval

Cited by

6 results in Mathlib

Foundations

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

Assumes

ZeroPartialOrderLocallyFiniteOrderDecidableEq