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.
Finitely supported product of finsets.
t is supported on
f ∈ s.dfinsupp t precisely means that
f is pointwise in
finset.singleton bundled as a
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