# Finite intervals of finitely supported functions #

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

def Finset.dfinsupp {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Zero (α i)] (s : ) (t : (i : ι) → Finset (α i)) :
Finset (Π₀ (i : ι), α i)

Finitely supported product of finsets.

Equations
• s.dfinsupp t = Finset.map { toFun := fun (f : (a : ι) → a sα a) => DFinsupp.mk s fun (i : s) => f i , inj' := } (s.pi t)
Instances For
@[simp]
theorem Finset.card_dfinsupp {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Zero (α i)] (s : ) (t : (i : ι) → Finset (α i)) :
(s.dfinsupp t).card = is, (t i).card
theorem Finset.mem_dfinsupp_iff {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Zero (α i)] {s : } {f : Π₀ (i : ι), α i} {t : (i : ι) → Finset (α i)} [(i : ι) → DecidableEq (α i)] :
f s.dfinsupp t f.support s is, f i t i
@[simp]
theorem Finset.mem_dfinsupp_iff_of_support_subset {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → Zero (α i)] {s : } {f : Π₀ (i : ι), α i} [(i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)} (ht : t.support s) :
f s.dfinsupp t ∀ (i : ι), f i t i

When t is supported on s, f ∈ s.dfinsupp t precisely means that f is pointwise in t.

def DFinsupp.singleton {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] (f : Π₀ (i : ι), α i) :
Π₀ (i : ι), Finset (α i)

Pointwise Finset.singleton bundled as a DFinsupp.

Equations
• f.singleton = { toFun := fun (i : ι) => {f i}, support' := Trunc.map (fun (s : { s : // ∀ (i : ι), i s f.toFun i = 0 }) => s, ) f.support' }
Instances For
theorem DFinsupp.mem_singleton_apply_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :
a f.singleton i a = f i
def DFinsupp.rangeIcc {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
Π₀ (i : ι), Finset (α i)

Pointwise Finset.Icc bundled as a DFinsupp.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem DFinsupp.rangeIcc_apply {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) (i : ι) :
(f.rangeIcc g) i = Finset.Icc (f i) (g i)
theorem DFinsupp.mem_rangeIcc_apply_iff {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} {i : ι} {a : α i} :
a (f.rangeIcc g) i f i a a g i
theorem DFinsupp.support_rangeIcc_subset {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f : Π₀ (i : ι), α i} {g : Π₀ (i : ι), α i} [] [(i : ι) → DecidableEq (α i)] :
(f.rangeIcc g).support f.support g.support
def DFinsupp.pi {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)) :
Finset (Π₀ (i : ι), α i)

Given a finitely supported function f : Π₀ i, Finset (α i), one can define the finset f.pi of all finitely supported functions whose value at i is in f i for all i.

Equations
• f.pi = f.support.dfinsupp f
Instances For
@[simp]
theorem DFinsupp.mem_pi {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → DecidableEq (α i)] {f : Π₀ (i : ι), Finset (α i)} {g : Π₀ (i : ι), α i} :
g f.pi ∀ (i : ι), g i f i
@[simp]
theorem DFinsupp.card_pi {ι : Type u_1} {α : ιType u_2} [(i : ι) → Zero (α i)] [] [(i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)) :
f.pi.card = f.prod fun (i : ι) => (f i).card
instance DFinsupp.instLocallyFiniteOrder {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] :
LocallyFiniteOrder (Π₀ (i : ι), α i)
Equations
• DFinsupp.instLocallyFiniteOrder = LocallyFiniteOrder.ofIcc (Π₀ (i : ι), α i) (fun (f g : Π₀ (i : ι), α i) => (f.support g.support).dfinsupp (f.rangeIcc g))
theorem DFinsupp.Icc_eq {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
= (f.support g.support).dfinsupp (f.rangeIcc g)
theorem DFinsupp.card_Icc {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
(Finset.Icc f g).card = if.support g.support, (Finset.Icc (f i) (g i)).card
theorem DFinsupp.card_Ico {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
(Finset.Ico f g).card = if.support g.support, (Finset.Icc (f i) (g i)).card - 1
theorem DFinsupp.card_Ioc {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
(Finset.Ioc f g).card = if.support g.support, (Finset.Icc (f i) (g i)).card - 1
theorem DFinsupp.card_Ioo {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
(Finset.Ioo f g).card = if.support g.support, (Finset.Icc (f i) (g i)).card - 2
theorem DFinsupp.card_uIcc {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → Lattice (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :
(Finset.uIcc f g).card = if.support g.support, (Finset.uIcc (f i) (g i)).card
theorem DFinsupp.card_Iic {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → ] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :
(Finset.Iic f).card = if.support, (Finset.Iic (f i)).card
theorem DFinsupp.card_Iio {ι : Type u_1} {α : ιType u_2} [] [(i : ι) → DecidableEq (α i)] [(i : ι) → ] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :
(Finset.Iio f).card = if.support, (Finset.Iic (f i)).card - 1