Documentation

Mathlib.Data.Finsupp.Interval

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 #

Both these definitions use the fact that 0 = {0} to ensure that the resulting function is finitely supported.

source
@[simp]
theorem Finsupp.rangeSingleton_toFun {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) (i : ι) :
(Finsupp.rangeSingleton f) i = {f i}
source
@[simp]
theorem Finsupp.rangeSingleton_support {ι : Type u_1} {α : Type u_2} [Zero α] (f : ι →₀ α) :
(Finsupp.rangeSingleton f).support = f.support
source
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) }
Instances For
    source
    theorem Finsupp.mem_rangeSingleton_apply_iff {ι : Type u_1} {α : Type u_2} [Zero α] {f : ι →₀ α} {i : ι} {a : α} :
    a ∈ (Finsupp.rangeSingleton f) i ↔ a = f i
    source
    @[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)
    source
    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.
    Instances For
      source
      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)
      source
      @[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
      source
      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
      source
      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.
      source
      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)
      source
      theorem Finsupp.card_Icc {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) :
      (Finset.Icc f g).card = Finset.prod (f.support ∪ g.support) fun (i : ι) => (Finset.Icc (f i) (g i)).card
      source
      theorem Finsupp.card_Ico {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) :
      (Finset.Ico f g).card = (Finset.prod (f.support ∪ g.support) fun (i : ι) => (Finset.Icc (f i) (g i)).card) - 1
      source
      theorem Finsupp.card_Ioc {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) :
      (Finset.Ioc f g).card = (Finset.prod (f.support ∪ g.support) fun (i : ι) => (Finset.Icc (f i) (g i)).card) - 1
      source
      theorem Finsupp.card_Ioo {ι : Type u_1} {α : Type u_2} [PartialOrder α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) :
      (Finset.Ioo f g).card = (Finset.prod (f.support ∪ g.support) fun (i : ι) => (Finset.Icc (f i) (g i)).card) - 2
      source
      theorem Finsupp.card_uIcc {ι : Type u_1} {α : Type u_2} [Lattice α] [Zero α] [LocallyFiniteOrder α] (f : ι →₀ α) (g : ι →₀ α) :
      (Finset.uIcc f g).card = Finset.prod (f.support ∪ g.support) fun (i : ι) => (Finset.uIcc (f i) (g i)).card
      source
      theorem Finsupp.card_Iic {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddCommMonoid α] [LocallyFiniteOrder α] (f : ι →₀ α) :
      (Finset.Iic f).card = Finset.prod f.support fun (i : ι) => (Finset.Iic (f i)).card
      source
      theorem Finsupp.card_Iio {ι : Type u_1} {α : Type u_2} [CanonicallyOrderedAddCommMonoid α] [LocallyFiniteOrder α] (f : ι →₀ α) :
      (Finset.Iio f).card = (Finset.prod f.support fun (i : ι) => (Finset.Iic (f i)).card) - 1