nonempty

Mathlib.Data.Fintype.EquivFin

URI: https://scilib.ai/kg/mathlib#Infinite.nonempty

English

Every infinite type is Nonempty.

Русский

Каждый бесконечный тип непуст.

LaTeX

$$[Infinite α] → Nonempty α$$

Lean4

protected theorem nonempty (α : Type*) [Infinite α] : Nonempty α := by infer_instance

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

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

Разделы

Аффилиация

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