# mathlibdocumentation

data.finsupp.interval

# Finite intervals of finitely supported functions #

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

## Main declarations #

• finsupp.range_singleton: Postcomposition with has_singleton.singleton on finset as a finsupp.
• finsupp.range_Icc: 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.range_singleton_to_fun {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) (i : ι) :
@[simp]
theorem finsupp.range_singleton_support {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) :
def finsupp.range_singleton {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) :
ι →₀

Pointwise finset.singleton bundled as a finsupp.

Equations
theorem finsupp.mem_range_singleton_apply_iff {ι : Type u_1} {α : Type u_2} [has_zero α] {f : ι →₀ α} {i : ι} {a : α} :
@[simp]
theorem finsupp.range_Icc_to_fun {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) (i : ι) :
(f.range_Icc g) i = finset.Icc (f i) (g i)
@[simp]
theorem finsupp.range_Icc_support {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
noncomputable def finsupp.range_Icc {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
ι →₀

Pointwise finset.Icc bundled as a finsupp.

Equations
theorem finsupp.mem_range_Icc_apply_iff {ι : Type u_1} {α : Type u_2} [has_zero α] {f g : ι →₀ α} {i : ι} {a : α} :
a (f.range_Icc g) i f i a a g i
@[protected, instance]
noncomputable def finsupp.locally_finite_order {ι : Type u_1} {α : Type u_2} [has_zero α]  :
Equations
theorem finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card)
theorem finsupp.card_Ico {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 1
theorem finsupp.card_Ioc {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 1
theorem finsupp.card_Ioo {ι : Type u_1} {α : Type u_2} [has_zero α] (f g : ι →₀ α) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 2