mathlib3 documentation

data.finsupp.interval

Finite intervals of finitely supported functions #

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

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)
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
@[simp]
theorem finsupp.range_Icc_support {ι : Type u_1} {α : Type u_2} [has_zero α] [partial_order α] [locally_finite_order α] [decidable_eq ι] (f g : ι →₀ α) :
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.Icc_eq {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
theorem finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
(finset.Icc f 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} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
(finset.Ico f 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} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
(finset.Ioc f 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} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
(finset.Ioo f g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 2
theorem finsupp.card_uIcc {ι : Type u_1} {α : Type u_2} [lattice α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :
(finset.uIcc f g).card = (f.support g.support).prod (λ (i : ι), (finset.uIcc (f i) (g i)).card)
theorem finsupp.card_Iic {ι : Type u_1} {α : Type u_2} [canonically_ordered_add_monoid α] [locally_finite_order α] (f : ι →₀ α) :
(finset.Iic f).card = f.support.prod (λ (i : ι), (finset.Iic (f i)).card)
theorem finsupp.card_Iio {ι : Type u_1} {α : Type u_2} [canonically_ordered_add_monoid α] [locally_finite_order α] (f : ι →₀ α) :
(finset.Iio f).card = f.support.prod (λ (i : ι), (finset.Iic (f i)).card) - 1