Documentation

Mathlib.Data.Finsupp.Indicator

Building finitely supported functions off finsets #

This file defines Finsupp.indicator to help create finsupps from finsets.

Main declarations #

def Finsupp.indicator {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i sα) :
ι →₀ α

Create an element of ι →₀ α from a finset s and a function f defined on this finset.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Finsupp.indicator_of_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : i s) (f : (i : ι) → i sα) :
    (Finsupp.indicator s f) i = f i hi
    theorem Finsupp.indicator_of_not_mem {ι : Type u_1} {α : Type u_2} [Zero α] {s : Finset ι} {i : ι} (hi : is) (f : (i : ι) → i sα) :
    @[simp]
    theorem Finsupp.indicator_apply {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i sα) (i : ι) [DecidableEq ι] :
    (Finsupp.indicator s f) i = if hi : i s then f i hi else 0
    theorem Finsupp.indicator_injective {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) :
    Function.Injective fun (f : (i : ι) → i sα) => Finsupp.indicator s f
    theorem Finsupp.support_indicator_subset {ι : Type u_1} {α : Type u_2} [Zero α] (s : Finset ι) (f : (i : ι) → i sα) :
    (Finsupp.indicator s f).support s
    theorem Finsupp.single_eq_indicator {ι : Type u_1} {α : Type u_2} [Zero α] (i : ι) (b : α) :
    Finsupp.single i b = Finsupp.indicator {i} fun (x : ι) (x : x {i}) => b