instCountableFin

Mathlib.Data.Countable.Defs

URI: https://scilib.ai/kg/mathlib#instCountableFin

English

For every n, Fin n is countable.

Русский

Для каждого n тип Fin n счётен.

LaTeX

$$$\forall n:\mathbb{N}, \text{Countable}(\mathrm{Fin}\;n)$$$

Lean4

instance {n : ℕ} : Countable (Fin n) :=
  Function.Injective.countable (@Fin.eq_of_val_eq n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru