# mathlib3documentation

data.dfinsupp.interval

# Finite intervals of finitely supported functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the locally_finite_order 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} [decidable_eq ι] [Π (i : ι), has_zero (α i)] (s : finset ι) (t : Π (i : ι), finset (α i)) :
finset (Π₀ (i : ι), α i)

Finitely supported product of finsets.

Equations
@[simp]
theorem finset.card_dfinsupp {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), has_zero (α i)] (s : finset ι) (t : Π (i : ι), finset (α i)) :
(s.dfinsupp t).card = s.prod (λ (i : ι), (t i).card)
theorem finset.mem_dfinsupp_iff {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), has_zero (α i)] {s : finset ι} {f : Π₀ (i : ι), α i} {t : Π (i : ι), finset (α i)} [Π (i : ι), decidable_eq (α i)] :
f s.dfinsupp t f.support s (i : ι), i s f i t i
@[simp]
theorem finset.mem_dfinsupp_iff_of_support_subset {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), has_zero (α i)] {s : finset ι} {f : Π₀ (i : ι), α i} [Π (i : ι), decidable_eq (α 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 : ι), has_zero (α i)] (f : Π₀ (i : ι), α i) :
Π₀ (i : ι), finset (α i)

Pointwise finset.singleton bundled as a dfinsupp.

Equations
theorem dfinsupp.mem_singleton_apply_iff {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :
a (f.singleton) i a = f i
def dfinsupp.range_Icc {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
Π₀ (i : ι), finset (α i)

Pointwise finset.Icc bundled as a dfinsupp.

Equations
@[simp]
theorem dfinsupp.range_Icc_apply {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
(f.range_Icc g) i = finset.Icc (f i) (g i)
theorem dfinsupp.mem_range_Icc_apply_iff {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] {f g : Π₀ (i : ι), α i} {i : ι} {a : α i} :
a (f.range_Icc g) i f i a a g i
theorem dfinsupp.support_range_Icc_subset {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), locally_finite_order (α i)] {f g : Π₀ (i : ι), α i} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] :
def dfinsupp.pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [decidable_eq ι] [Π (i : ι), decidable_eq (α 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
@[simp]
theorem dfinsupp.mem_pi {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), has_zero (α i)] [decidable_eq ι] [Π (i : ι), decidable_eq (α 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 : ι), has_zero (α i)] [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] (f : Π₀ (i : ι), finset (α i)) :
f.pi.card = f.prod (λ (i : ι), ((f i).card))
@[protected, instance]
def dfinsupp.locally_finite_order {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] :
Equations
theorem dfinsupp.Icc_eq {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
theorem dfinsupp.card_Icc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card)
theorem dfinsupp.card_Ico {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 1
theorem dfinsupp.card_Ioc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 1
theorem dfinsupp.card_Ioo {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), partial_order (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.Icc (f i) (g i)).card) - 2
theorem dfinsupp.card_uIcc {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), lattice (α i)] [Π (i : ι), has_zero (α i)] [Π (i : ι), locally_finite_order (α i)] (f g : Π₀ (i : ι), α i) :
g).card = (f.support g.support).prod (λ (i : ι), (finset.uIcc (f i) (g i)).card)
theorem dfinsupp.card_Iic {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), ] [Π (i : ι), locally_finite_order (α i)] (f : Π₀ (i : ι), α i) :
(finset.Iic f).card = f.support.prod (λ (i : ι), (finset.Iic (f i)).card)
theorem dfinsupp.card_Iio {ι : Type u_1} {α : ι Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), ] [Π (i : ι), locally_finite_order (α i)] (f : Π₀ (i : ι), α i) :
(finset.Iio f).card = f.support.prod (λ (i : ι), (finset.Iic (f i)).card) - 1