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.

source

@[simp]

theorem finsupp.range_singleton_to_fun {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) (i : ι) :

⇑(f.range_singleton) i = {⇑f i}

source

@[simp]

theorem finsupp.range_singleton_support {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) :

f.range_singleton.support = f.support

source

def finsupp.range_singleton {ι : Type u_1} {α : Type u_2} [has_zero α] (f : ι →₀ α) :

ι →₀ finset α

Pointwise finset.singleton bundled as a finsupp.

Equations

f.range_singleton = {support := f.support, to_fun := λ (i : ι), {⇑f i}, mem_support_to_fun := _}

source

theorem finsupp.mem_range_singleton_apply_iff {ι : Type u_1} {α : Type u_2} [has_zero α] {f : ι →₀ α} {i : ι} {a : α} :

a ∈ ⇑(f.range_singleton) i ↔ a = ⇑f i

source

@[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)

source

@[simp]

theorem finsupp.range_Icc_support {ι : Type u_1} {α : Type u_2} [has_zero α] [partial_order α] [locally_finite_order α] (f g : ι →₀ α) :

(f.range_Icc g).support = f.support ∪ g.support

source

noncomputable def finsupp.range_Icc {ι : Type u_1} {α : Type u_2} [has_zero α] [partial_order α] [locally_finite_order α] (f g : ι →₀ α) :

ι →₀ finset α

Pointwise finset.Icc bundled as a finsupp.

Equations

f.range_Icc g = {support := f.support ∪ g.support, to_fun := λ (i : ι), finset.Icc (⇑f i) (⇑g i), mem_support_to_fun := _}

source

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

source

@[protected, instance]

noncomputable def finsupp.locally_finite_order {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] :

locally_finite_order (ι →₀ α)

Equations

finsupp.locally_finite_order = locally_finite_order.of_Icc (ι →₀ α) (λ (f g : ι →₀ α), (f.support ∪ g.support).finsupp ⇑(f.range_Icc g)) finsupp.locally_finite_order._proof_1

source

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

source

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

source

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

source

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