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 #

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

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

@[simp]

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

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

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.Icc_eq {ι : Type u_1} {α : Type u_2} [partial_order α] [has_zero α] [locally_finite_order α] (f g : ι →₀ α) [decidable_eq ι] :

finset.Icc f g = (f.support ∪ g.support).finsupp ⇑(f.range_Icc g)

source

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)

source

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

source

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

source

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

source

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)

source

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)

source

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