fintype — Mathlib

English

There is a Fintype instance for DFinsupp Π₀ i, π i whenever ι is finite and each π i is finite.

Русский

Существует экземпляр Finite для DFinsupp Π₀ i, π i, если ι конечен и каждый π i конечен.

LaTeX

$$$\\text{Fintype}(DFinsupp\\; f) \\text{ при } ι\\text{ конечен и } ∀ i,\\; Fintype(π i)$$$

Lean4

instance fintype {ι : Sort _} {π : ι → Sort _} [DecidableEq ι] [∀ i, Zero (π i)] [Fintype ι] [∀ i, Fintype (π i)] :
    Fintype (Π₀ i, π i) :=
  Fintype.ofEquiv (∀ i, π i) DFinsupp.equivFunOnFintype.symm

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