Mathlib.Data.Finsupp.Fintype

Module docstring

{"# Finiteness and infiniteness of Finsupp

Some lemmas on the combination of Finsupp, Fintype and Infinite.

Finsupp.fintype instance

: Fintype (ι →₀ α)

Full source

noncomputable instance Finsupp.fintype : Fintype (ι →₀ α) :=
  Fintype.ofEquiv _ Finsupp.equivFunOnFinite.symm

Finiteness of Finitely Supported Functions on Finite Types

Informal description

For any finite type $\iota$ and any type $\alpha$ with a zero element, the type of finitely supported functions $\iota \to₀ \alpha$ is finite.

Finsupp.infinite_of_left instance

[Nontrivial α] [Infinite ι] : Infinite (ι →₀ α)

Full source

instance Finsupp.infinite_of_left [Nontrivial α] [Infinite ι] : Infinite (ι →₀ α) :=
  let ⟨_, hm⟩ := exists_ne (0 : α)
  Infinite.of_injective _ <| Finsupp.single_left_injective hm

Infinite Domain Yields Infinite Finitely Supported Functions

Informal description

For any nontrivial type $\alpha$ with a zero element and any infinite type $\iota$, the type of finitely supported functions $\iota \to₀ \alpha$ is infinite.

Finsupp.infinite_of_right instance

[Infinite α] [Nonempty ι] : Infinite (ι →₀ α)

Full source

instance Finsupp.infinite_of_right [Infinite α] [Nonempty ι] : Infinite (ι →₀ α) :=
  Infinite.of_injective (fun i => Finsupp.single (Classical.arbitrary ι) i)
    (Finsupp.single_injective (Classical.arbitrary ι))

Infinite Type Yields Infinite Finitely Supported Functions

Informal description

For any infinite type $\alpha$ with a zero element and any nonempty type $\iota$, the type of finitely supported functions $\iota \to₀ \alpha$ is infinite.

Fintype.card_finsupp theorem

: card (ι →₀ α) = card α ^ card ι

Full source

@[simp] lemma Fintype.card_finsupp : card (ι →₀ α) = card α ^ card ι := by
  simp [card_congr Finsupp.equivFunOnFinite]

Cardinality of Finitely Supported Functions: $|\iota \to₀ \alpha| = |\alpha|^{|\iota|}$

Informal description

For any finite types $\iota$ and $\alpha$ (where $\alpha$ has a zero element), the number of finitely supported functions from $\iota$ to $\alpha$ is equal to $|\alpha|^{|\iota|}$, where $|\cdot|$ denotes the cardinality of a finite set.