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.

source

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

Finset (Π₀ (i : ι), α i)

Finitely supported product of finsets.

Instances For

source

@[simp]

theorem Finset.card_dfinsupp {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :

Finset.card (Finset.dfinsupp s t) = Finset.prod s fun i => Finset.card (t i)

source

theorem Finset.mem_dfinsupp_iff {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : Π₀ (i : ι), α i} {t : (i : ι) → Finset (α i)} [(i : ι) → DecidableEq (α i)] :

f ∈ Finset.dfinsupp s t ↔ DFinsupp.support f ⊆ s ∧ ∀ (i : ι), i ∈ s → ↑f i ∈ t i

source

@[simp]

theorem Finset.mem_dfinsupp_iff_of_support_subset {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : Π₀ (i : ι), α i} [(i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)} (ht : DFinsupp.support t ⊆ s) :

f ∈ Finset.dfinsupp s ↑t ↔ ∀ (i : ι), ↑f i ∈ ↑t i

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

source

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.

Instances For

source

theorem DFinsupp.mem_singleton_apply_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :

a ∈ ↑(DFinsupp.singleton f) i ↔ a = ↑f i

source

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.

Instances For

source

@[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 : ι) :

↑(DFinsupp.rangeIcc f g) i = Finset.Icc (↑f i) (↑g i)

source

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 ∈ ↑(DFinsupp.rangeIcc f g) i ↔ ↑f i ≤ a ∧ a ≤ ↑g i

source

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} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] :

DFinsupp.support (DFinsupp.rangeIcc f g) ⊆ DFinsupp.support f ∪ DFinsupp.support g

source

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

Instances For

source

@[simp]

theorem DFinsupp.mem_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] {f : Π₀ (i : ι), Finset (α i)} {g : Π₀ (i : ι), α i} :

g ∈ DFinsupp.pi f ↔ ∀ (i : ι), ↑g i ∈ ↑f i

source

@[simp]

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

Finset.card (DFinsupp.pi f) = DFinsupp.prod f fun i => ↑(Finset.card (↑f i))

source

instance DFinsupp.instLocallyFiniteOrderDFinsuppInstPreorderDFinsuppToPreorder {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] :

LocallyFiniteOrder (Π₀ (i : ι), α i)

source

theorem DFinsupp.Icc_eq {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.Icc f g = Finset.dfinsupp (DFinsupp.support f ∪ DFinsupp.support g) ↑(DFinsupp.rangeIcc f g)

source

theorem DFinsupp.card_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.card (Finset.Icc f g) = Finset.prod (DFinsupp.support f ∪ DFinsupp.support g) fun i => Finset.card (Finset.Icc (↑f i) (↑g i))

source

theorem DFinsupp.card_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.card (Finset.Ico f g) = (Finset.prod (DFinsupp.support f ∪ DFinsupp.support g) fun i => Finset.card (Finset.Icc (↑f i) (↑g i))) - 1

source

theorem DFinsupp.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.card (Finset.Ioc f g) = (Finset.prod (DFinsupp.support f ∪ DFinsupp.support g) fun i => Finset.card (Finset.Icc (↑f i) (↑g i))) - 1

source

theorem DFinsupp.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.card (Finset.Ioo f g) = (Finset.prod (DFinsupp.support f ∪ DFinsupp.support g) fun i => Finset.card (Finset.Icc (↑f i) (↑g i))) - 2

source

theorem DFinsupp.card_uIcc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Lattice (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) (g : Π₀ (i : ι), α i) :

Finset.card (Finset.uIcc f g) = Finset.prod (DFinsupp.support f ∪ DFinsupp.support g) fun i => Finset.card (Finset.uIcc (↑f i) (↑g i))

source

theorem DFinsupp.card_Iic {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → CanonicallyOrderedAddMonoid (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :

Finset.card (Finset.Iic f) = Finset.prod (DFinsupp.support f) fun i => Finset.card (Finset.Iic (↑f i))

source

theorem DFinsupp.card_Iio {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → CanonicallyOrderedAddMonoid (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :

Finset.card (Finset.Iio f) = (Finset.prod (DFinsupp.support f) fun i => Finset.card (Finset.Iic (↑f i))) - 1