instCountableFinsupp — Mathlib

English

If α and β are countable and β has a zero, then the set of finitely supported functions α →₀ β is countable.

Русский

Если α и β счетны и β имеет нуль, то множество функций с конечной опорой α →₀ β счетно.

LaTeX

$$$\\forall {\\alpha \\beta} [\\text{Countable }\\alpha] [\\text{Countable }\\beta] [Zero \\beta],\\ Countable (\\alpha \\to_0 \\beta)$$$

Lean4

instance {α β : Type*} [Countable α] [Countable β] [Zero β] : Countable (α →₀ β) := by
  classical exact .of_equiv _ finsuppEquivDFinsupp.symm

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