mathlib documentation

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 #

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 α] [partial_order α] [locally_finite_order α] (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 α] [partial_order α] [locally_finite_order α] (f g : ι →₀ α) :
noncomputable def finsupp.range_Icc {ι : Type u_1} {α : Type u_2} [has_zero α] [partial_order α] [locally_finite_order α] (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 α] [partial_order α] [locally_finite_order α] {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} [partial_order α] [has_zero α] [locally_finite_order α] :
Equations
theorem finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) :
(finset.Icc f g).card = ∏ (i : ι) in f.support g.support, (finset.Icc (f i) (g i)).card
theorem finsupp.card_Ico {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) :
(finset.Ico f g).card = ∏ (i : ι) in f.support g.support, (finset.Icc (f i) (g i)).card - 1
theorem finsupp.card_Ioc {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) :
(finset.Ioc f g).card = ∏ (i : ι) in f.support g.support, (finset.Icc (f i) (g i)).card - 1
theorem finsupp.card_Ioo {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) :
(finset.Ioo f g).card = ∏ (i : ι) in f.support g.support, (finset.Icc (f i) (g i)).card - 2