instInfiniteListOfNonempty

Mathlib.Data.Fintype.EquivFin

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

English

If α is nonempty, then List α is infinite.

Русский

Если α непусто, то List α бесконечен.

LaTeX

$$[Nonempty α] ⇒ Infinite (List α)$$

Lean4

instance [Nonempty α] : Infinite (List α) :=
  Infinite.of_surjective ((↑) : List α → Multiset α) Quot.mk_surjective

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

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

Разделы

Аффилиация

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