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.

@[simp]

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

@[simp]

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

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

Pointwise Singleton.singleton bundled as a Finsupp.

Equations

• Finsupp.rangeSingleton f = { support := f.support, toFun := fun i => {↑f i}, mem_support_toFun := (_ : ∀ (i : ι), i ∈ f.support ↔ (fun i => {↑f i}) i ≠ 0) }

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

@[simp]

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

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

Pointwise Finset.Icc bundled as a Finsupp.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem Finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) : Finset.card (Finset.Icc f g) = Finset.prod (f.support ∪ g.support) fun i => Finset.card (Finset.Icc (↑f i) (↑g i))

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

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

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

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

theorem Finsupp.card_Iic {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [LocallyFiniteOrder α] (f : ι →₀ α) : Finset.card (Finset.Iic f) = Finset.prod f.support fun i => Finset.card (Finset.Iic (↑f i))

theorem Finsupp.card_Iio {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddMonoid α] [LocallyFiniteOrder α] (f : ι →₀ α) : Finset.card (Finset.Iio f) = (Finset.prod f.support fun i => Finset.card (Finset.Iic (↑f i))) - 1