fintype — Mathlib

English

If ι is finite and α is finite with a zero, then the type of finitely supported functions ι →₀ α is finite (i.e., there exists a finite Fintype structure on ι →₀ α).

Русский

Если ι конечно, а α конечно и имеет нулевой элемент, то множество конечноподдерживаемых функций ι →₀ α конечное.

LaTeX

$$$\\#(ι \\to_0 α) < \\infty$$$

Lean4

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

Похожие утверждения