exists_equiv_fin

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Finite.exists_equiv_fin

English

If α is finite, then there exists n such that α is bijectively equivalent to Fin n.

Русский

Если α конечно, то существует n такое, что α эквивалентно Fin n.

LaTeX

$$$\text{Finite}(\\alpha) \\iff \\exists n \\in \\mathbb{N}, \\text{Nonempty}(\\alpha \\simeq \\mathrm{Fin}(n)).$$$

Lean4

theorem exists_equiv_fin (α : Sort*) [h : Finite α] : ∃ n : ℕ, Nonempty (α ≃ Fin n) :=
  finite_iff_exists_equiv_fin.mp h

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

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

Разделы

Аффилиация

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