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} [DecidableEq ι] [(i : ι) → Zero (α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) : Finset (DFinsupp fun (i : ι) => α i)

Finitely supported product of finsets.

Equations

• Eq (s.dfinsupp t) (Finset.map { toFun := fun (f : (a : ι) → Membership.mem s a → α a) => DFinsupp.mk s fun (i : s.toSet.Elem) => f i.val ⋯, inj' := ⋯ } (s.pi t))

theorem Finset.card_dfinsupp {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) : Eq (s.dfinsupp t).card (s.prod fun (i : ι) => (t i).card)

theorem Finset.mem_dfinsupp_iff {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : DFinsupp fun (i : ι) => α i} {t : (i : ι) → Finset (α i)} [(i : ι) → DecidableEq (α i)] : Iff (Membership.mem (s.dfinsupp t) f) (And (HasSubset.Subset f.support s) (∀ (i : ι), Membership.mem s i → Membership.mem (t i) (DFunLike.coe f i)))

theorem Finset.mem_dfinsupp_iff_of_support_subset {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : DFinsupp fun (i : ι) => α i} [(i : ι) → DecidableEq (α i)] {t : DFinsupp fun (i : ι) => Finset (α i)} (ht : HasSubset.Subset t.support s) : Iff (Membership.mem (s.dfinsupp (DFunLike.coe t)) f) (∀ (i : ι), Membership.mem (DFunLike.coe t i) (DFunLike.coe f 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 : DFinsupp fun (i : ι) => α i) : DFinsupp fun (i : ι) => Finset (α i)

Pointwise Finset.singleton bundled as a DFinsupp.

Equations

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

theorem DFinsupp.mem_singleton_apply_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {f : DFinsupp fun (i : ι) => α i} {i : ι} {a : α i} : Iff (Membership.mem (DFunLike.coe f.singleton i) a) (Eq a (DFunLike.coe f i))

def DFinsupp.rangeIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : DFinsupp fun (i : ι) => Finset (α i)

Pointwise Finset.Icc bundled as a DFinsupp.

Equations

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

theorem DFinsupp.rangeIcc_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) (i : ι) : Eq (DFunLike.coe (f.rangeIcc g) i) (Finset.Icc (DFunLike.coe f i) (DFunLike.coe g i))

theorem DFinsupp.mem_rangeIcc_apply_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f g : DFinsupp fun (i : ι) => α i} {i : ι} {a : α i} : Iff (Membership.mem (DFunLike.coe (f.rangeIcc g) i) a) (And (LE.le (DFunLike.coe f i) a) (LE.le a (DFunLike.coe g i)))

theorem DFinsupp.support_rangeIcc_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f g : DFinsupp fun (i : ι) => α i} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] : HasSubset.Subset (f.rangeIcc g).support (Union.union f.support g.support)

def DFinsupp.pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] (f : DFinsupp fun (i : ι) => Finset (α i)) : Finset (DFinsupp fun (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

• Eq f.pi (f.support.dfinsupp (DFunLike.coe f))

theorem DFinsupp.mem_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] {f : DFinsupp fun (i : ι) => Finset (α i)} {g : DFinsupp fun (i : ι) => α i} : Iff (Membership.mem f.pi g) (∀ (i : ι), Membership.mem (DFunLike.coe f i) (DFunLike.coe g i))

theorem DFinsupp.card_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] (f : DFinsupp fun (i : ι) => Finset (α i)) : Eq f.pi.card (f.prod fun (i : ι) => (DFunLike.coe f i).card.cast)

def DFinsupp.instLocallyFiniteOrder {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] : LocallyFiniteOrder (DFinsupp fun (i : ι) => α i)

Equations

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

theorem DFinsupp.Icc_eq {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.Icc f g) ((Union.union f.support g.support).dfinsupp (DFunLike.coe (f.rangeIcc g)))

theorem DFinsupp.card_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.Icc f g).card ((Union.union f.support g.support).prod fun (i : ι) => (Finset.Icc (DFunLike.coe f i) (DFunLike.coe g i)).card)

theorem DFinsupp.card_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.Ico f g).card (HSub.hSub ((Union.union f.support g.support).prod fun (i : ι) => (Finset.Icc (DFunLike.coe f i) (DFunLike.coe g i)).card) 1)

theorem DFinsupp.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.Ioc f g).card (HSub.hSub ((Union.union f.support g.support).prod fun (i : ι) => (Finset.Icc (DFunLike.coe f i) (DFunLike.coe g i)).card) 1)

theorem DFinsupp.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.Ioo f g).card (HSub.hSub ((Union.union f.support g.support).prod fun (i : ι) => (Finset.Icc (DFunLike.coe f i) (DFunLike.coe g i)).card) 2)

theorem DFinsupp.card_uIcc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Lattice (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : DFinsupp fun (i : ι) => α i) : Eq (Finset.uIcc f g).card ((Union.union f.support g.support).prod fun (i : ι) => (Finset.uIcc (DFunLike.coe f i) (DFunLike.coe g i)).card)

theorem DFinsupp.card_Iic {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : DFinsupp fun (i : ι) => α i) : Eq (Finset.Iic f).card (f.support.prod fun (i : ι) => (Finset.Iic (DFunLike.coe f i)).card)

theorem DFinsupp.card_Iio {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : DFinsupp fun (i : ι) => α i) : Eq (Finset.Iio f).card (HSub.hSub (f.support.prod fun (i : ι) => (Finset.Iic (DFunLike.coe f i)).card) 1)