mathlib3 documentation

data.finsupp.indicator

Building finitely supported functions off finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

noncomputable def finsupp.indicator {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (f : Π (i : ι), i s α) :
ι →₀ α

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

Equations
theorem finsupp.indicator_of_mem {ι : Type u_1} {α : Type u_2} [has_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} [has_zero α] {s : finset ι} {i : ι} (hi : i s) (f : Π (i : ι), i s α) :
@[simp]
theorem finsupp.indicator_apply {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (f : Π (i : ι), i s α) (i : ι) [decidable_eq ι] :
(finsupp.indicator s f) i = dite (i s) (λ (hi : i s), f i hi) (λ (hi : i s), 0)
theorem finsupp.indicator_injective {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) :
function.injective (λ (f : Π (i : ι), i s α), finsupp.indicator s f)
theorem finsupp.support_indicator_subset {ι : Type u_1} {α : Type u_2} [has_zero α] (s : finset ι) (f : Π (i : ι), i s α) :
theorem finsupp.single_eq_indicator {ι : Type u_1} {α : Type u_2} [has_zero α] (i : ι) (b : α) :
finsupp.single i b = finsupp.indicator {i} (λ (_x : ι) (_x : _x {i}), b)