Finite intervals of finitely supported functions

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

Main declarations

• Finsupp.rangeSingleton: Postcomposition with Singleton.singleton on Finset as a Finsupp.
• Finsupp.rangeIcc: 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.

def Finsupp.rangeSingleton {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) : ι →₀ Finset α

Pointwise Singleton.singleton bundled as a Finsupp.

Equations

• f.rangeSingleton = { support := f.support, toFun := fun (i : ι) => {f i}, mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.rangeSingleton_support {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) : f.rangeSingleton.support = f.support

@[simp]

theorem Finsupp.rangeSingleton_apply {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) (i : ι) : f.rangeSingleton i = {f i}

theorem Finsupp.mem_rangeSingleton_apply_iff {ι : Type u_1} {α : Type u_2} [Zero α] {f : ι →₀ α} {i : ι} {a : α} : a ∈ f.rangeSingleton i ↔ a = f i

def Finsupp.rangeIcc {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq ι] (f g : ι →₀ α) : ι →₀ Finset α

Pointwise Finset.Icc bundled as a Finsupp.

Equations

• f.rangeIcc g = { support := f.support ∪ g.support, toFun := fun (i : ι) => Finset.Icc (f i) (g i), mem_support_toFun := ⋯ }

@[simp]

theorem Finsupp.rangeIcc_apply {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq ι] (f g : ι →₀ α) (i : ι) : (f.rangeIcc g) i = Finset.Icc (f i) (g i)

theorem Finsupp.coe_rangeIcc {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq ι] {i : ι} (f g : ι →₀ α) : (f.rangeIcc g) i = Finset.Icc (f i) (g i)

@[simp]

theorem Finsupp.rangeIcc_support {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq ι] (f g : ι →₀ α) : (f.rangeIcc g).support = f.support ∪ g.support

theorem Finsupp.mem_rangeIcc_apply_iff {ι : Type u_1} {α : Type u_2} [Zero α] [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq ι] {f g : ι →₀ α} {i : ι} {a : α} : a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i

@[instance_reducible]

noncomputable instance Finsupp.instLocallyFiniteOrder {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] : LocallyFiniteOrder (ι →₀ α)

Equations

• Finsupp.instLocallyFiniteOrder = LocallyFiniteOrder.ofIcc (ι →₀ α) (fun (f g : ι →₀ α) => (f.support ∪ g.support).finsupp ⇑(f.rangeIcc g)) ⋯

theorem Finsupp.Icc_eq {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f g : ι →₀ α) : Finset.Icc f g = (f.support ∪ g.support).finsupp ⇑(f.rangeIcc g)

theorem Finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f g : ι →₀ α) : (Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card

theorem Finsupp.card_Ico {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f g : ι →₀ α) : (Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1

theorem Finsupp.card_Ioc {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f g : ι →₀ α) : (Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1

theorem Finsupp.card_Ioo {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f g : ι →₀ α) : (Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2

theorem Finsupp.card_uIcc {ι : Type u_1} {α : Type u_2} [Lattice α] [Zero α] [LocallyFiniteOrder α] (f g : ι →₀ α) : (Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card

theorem Finsupp.card_Iic {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α] [OrderBot α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f : ι →₀ α) : (Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card

theorem Finsupp.card_Iio {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [PartialOrder α] [IsBotZeroClass α] [OrderBot α] [LocallyFiniteOrder α] [DecidableEq ι] [DecidableEq α] (f : ι →₀ α) : (Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1