# Finite intervals of finitely supported functions #

This file provides the LocallyFiniteOrder instance for ι →₀ α when α itself is locally finite and calculates the cardinality of its finite intervals.

## Main declarations #

• Finsupp.rangeSingleton: Postcomposition with Singleton.singleton on Finset as a Finsupp.
• Finsupp.rangeIcc: Postcomposition with Finset.Icc as a Finsupp.

Both these definitions use the fact that 0 = {0} to ensure that the resulting function is finitely supported.

@[simp]
theorem Finsupp.rangeSingleton_toFun {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) (i : ι) :
f.rangeSingleton i = {f i}
@[simp]
theorem Finsupp.rangeSingleton_support {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) :
f.rangeSingleton.support = f.support
def Finsupp.rangeSingleton {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) :
ι →₀

Pointwise Singleton.singleton bundled as a Finsupp.

Equations
• f.rangeSingleton = { support := f.support, toFun := fun (i : ι) => {f i}, mem_support_toFun := }
Instances For
theorem Finsupp.mem_rangeSingleton_apply_iff {ι : Type u_1} {α : Type u_2} [Zero α] {f : ι →₀ α} {i : ι} {a : α} :
a f.rangeSingleton i a = f i
@[simp]
theorem Finsupp.rangeIcc_toFun {ι : Type u_1} {α : Type u_2} [Zero α] [] (f : ι →₀ α) (g : ι →₀ α) (i : ι) :
(f.rangeIcc g) i = Finset.Icc (f i) (g i)
def Finsupp.rangeIcc {ι : Type u_1} {α : Type u_2} [Zero α] [] (f : ι →₀ α) (g : ι →₀ α) :
ι →₀

Pointwise Finset.Icc bundled as a Finsupp.

Equations
• f.rangeIcc g = { support := f.support g.support, toFun := fun (i : ι) => Finset.Icc (f i) (g i), mem_support_toFun := }
Instances For
theorem Finsupp.coe_rangeIcc {ι : Type u_1} {α : Type u_2} [Zero α] [] {i : ι} (f : ι →₀ α) (g : ι →₀ α) :
(f.rangeIcc g) i = Finset.Icc (f i) (g i)
@[simp]
theorem Finsupp.rangeIcc_support {ι : Type u_1} {α : Type u_2} [Zero α] [] (f : ι →₀ α) (g : ι →₀ α) :
(f.rangeIcc g).support = f.support g.support
theorem Finsupp.mem_rangeIcc_apply_iff {ι : Type u_1} {α : Type u_2} [Zero α] [] {f : ι →₀ α} {g : ι →₀ α} {i : ι} {a : α} :
a (f.rangeIcc g) i f i a a g i
instance Finsupp.instLocallyFiniteOrder {ι : Type u_1} {α : Type u_2} [] [Zero α] :
Equations
theorem Finsupp.Icc_eq {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
= (f.support g.support).finsupp (f.rangeIcc g)
theorem Finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
().card = if.support g.support, (Finset.Icc (f i) (g i)).card
theorem Finsupp.card_Ico {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
().card = if.support g.support, (Finset.Icc (f i) (g i)).card - 1
theorem Finsupp.card_Ioc {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
().card = if.support g.support, (Finset.Icc (f i) (g i)).card - 1
theorem Finsupp.card_Ioo {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
().card = if.support g.support, (Finset.Icc (f i) (g i)).card - 2
theorem Finsupp.card_uIcc {ι : Type u_1} {α : Type u_2} [] [Zero α] (f : ι →₀ α) (g : ι →₀ α) :
().card = if.support g.support, (Finset.uIcc (f i) (g i)).card
theorem Finsupp.card_Iic {ι : Type u_1} {α : Type u_2} (f : ι →₀ α) :
().card = if.support, (Finset.Iic (f i)).card
theorem Finsupp.card_Iio {ι : Type u_1} {α : Type u_2} (f : ι →₀ α) :
().card = if.support, (Finset.Iic (f i)).card - 1