Finiteness and infiniteness of the DFinsupp type

Main results

• DFinsupp.fintype: if the domain and codomain are finite, then DFinsupp is finite
• DFinsupp.infinite_of_left: if the domain is infinite, then DFinsupp is infinite
• DFinsupp.infinite_of_exists_right: if one fiber of the codomain is infinite, then DFinsupp is infinite

@[instance_reducible]

instance DFinsupp.fintype {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (π i)] [Fintype ι] [(i : ι) → Fintype (π i)] : Fintype (Π₀ (i : ι), π i)

Equations

• DFinsupp.fintype = Fintype.ofEquiv ((i : ι) → π i) DFinsupp.equivFunOnFintype.symm

instance DFinsupp.infinite_of_left {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Nontrivial (π i)] [(i : ι) → Zero (π i)] [Infinite ι] : Infinite (Π₀ (i : ι), π i)

theorem DFinsupp.infinite_of_exists_right {ι : Type u_1} {π : ι → Type u_2} (i : ι) [Infinite (π i)] [(i : ι) → Zero (π i)] : Infinite (Π₀ (i : ι), π i)

See DFinsupp.infinite_of_right for this in instance form, with the drawback that it needs all π i to be infinite.

instance DFinsupp.infinite_of_right {ι : Type u_1} {π : ι → Type u_2} [∀ (i : ι), Infinite (π i)] [(i : ι) → Zero (π i)] [Nonempty ι] : Infinite (Π₀ (i : ι), π i)

See DFinsupp.infinite_of_exists_right for the case that only one π ι is infinite.