mathlib3 documentation

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.

source
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
source
@[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)
source
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
source
@[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.

source
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
source
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
source
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
source
@[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)
source
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
source
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)] :
(f.range_Icc g).support ⊆ f.support ∪ g.support
source
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
source
@[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
source
@[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))
source
@[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)] :
locally_finite_order (Π₀ (i : ι), α i)
Equations
source
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) :
finset.Icc f g = (f.support ∪ g.support).dfinsupp ⇑(f.range_Icc g)
source
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) :
(finset.Icc f g).card = (f.support ∪ g.support).prod (λ (i : ι), (finset.Icc (⇑f i) (⇑g i)).card)
source
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) :
(finset.Ico f g).card = (f.support ∪ g.support).prod (λ (i : ι), (finset.Icc (⇑f i) (⇑g i)).card) - 1
source
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) :
(finset.Ioc f g).card = (f.support ∪ g.support).prod (λ (i : ι), (finset.Icc (⇑f i) (⇑g i)).card) - 1
source
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) :
(finset.Ioo f g).card = (f.support ∪ g.support).prod (λ (i : ι), (finset.Icc (⇑f i) (⇑g i)).card) - 2
source
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) :
(finset.uIcc f g).card = (f.support ∪ g.support).prod (λ (i : ι), (finset.uIcc (⇑f i) (⇑g i)).card)
source
theorem dfinsupp.card_Iic {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), locally_finite_order (α i)] (f : Π₀ (i : ι), α i) :
(finset.Iic f).card = f.support.prod (λ (i : ι), (finset.Iic (⇑f i)).card)
source
theorem dfinsupp.card_Iio {ι : Type u_1} {α : ι → Type u_2} [decidable_eq ι] [Π (i : ι), decidable_eq (α i)] [Π (i : ι), canonically_ordered_add_monoid (α i)] [Π (i : ι), locally_finite_order (α i)] (f : Π₀ (i : ι), α i) :
(finset.Iio f).card = f.support.prod (λ (i : ι), (finset.Iic (⇑f i)).card) - 1