Finite intervals of finitely supported functions #
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.
@[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) :
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}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
(f : Π₀ (i : ι), α i) :
Π₀ (i : ι), finset (α i)
Pointwise finset.singleton
bundled as a dfinsupp
.
theorem
dfinsupp.mem_singleton_apply_iff
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
{f : Π₀ (i : ι), α i}
{i : ι}
{a : α i} :
def
dfinsupp.range_Icc
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (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
.
@[simp]
theorem
dfinsupp.range_Icc_apply
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), locally_finite_order (α i)]
(f g : Π₀ (i : ι), α i)
(i : ι) :
theorem
dfinsupp.mem_range_Icc_apply_iff
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), locally_finite_order (α i)]
{f g : Π₀ (i : ι), α i}
{i : ι}
{a : α i} :
theorem
dfinsupp.support_range_Icc_subset
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
[Π (i : ι), partial_order (α i)]
[Π (i : ι), locally_finite_order (α i)]
{f g : Π₀ (i : ι), α i} :
def
dfinsupp.pi
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α 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
.
@[simp]
theorem
dfinsupp.mem_pi
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
{f : Π₀ (i : ι), finset (α i)}
{g : Π₀ (i : ι), α i} :
@[simp]
theorem
dfinsupp.card_pi
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), decidable_eq (α i)]
[Π (i : ι), has_zero (α i)]
(f : Π₀ (i : ι), finset (α i)) :
@[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
- dfinsupp.locally_finite_order = locally_finite_order.of_Icc (Π₀ (i : ι), α i) (λ (f g : Π₀ (i : ι), α i), (f.support ∪ g.support).dfinsupp ⇑(f.range_Icc g)) dfinsupp.locally_finite_order._proof_1
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) :
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) :
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) :
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) :