instFinite

Mathlib.Order.Atoms.Finite

URI: https://scilib.ai/kg/mathlib#IsSimpleOrder.instFinite

English

If α is a simple order with a finite structure, then α is finite.

Русский

Если алфавит простого порядка имеет конечную структуру, значит он конечен.

LaTeX

$$$\\text{Finite}(α) \\Rightarrow \\text{IsFinite}(α)$$$

Lean4

scoped instance (priority := 200) : Finite α := by classical infer_instance

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

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

Разделы

Аффилиация

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