instInfiniteMultisetOfNonempty

Mathlib.Data.Fintype.EquivFin

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

← MathLib Explorer

English

If α is nonempty, then the multiset α is infinite.

Русский

Если α непусто, то мультимножество α бесконечно.

LaTeX

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

Lean4

instance [Nonempty α] : Infinite (Multiset α) :=
  let ⟨x⟩ := ‹Nonempty α›
  Infinite.of_injective (fun n => Multiset.replicate n x) (Multiset.replicate_left_injective _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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