fintype

Mathlib.Data.Fintype.Defs

URI: https://scilib.ai/kg/mathlib#Ordering.fintype

English

The type Ordering consisting of the values LT, EQ, GT is finite (it has exactly three elements).

Русский

Тип Ordering, имеющий значения LT, EQ, GT, конечен (у него ровно три элемента).

LaTeX

$$$\mathrm{Ordering} \cong \mathrm{Fin}(3).$$$

Lean4

instance fintype : Fintype Ordering :=
  ⟨⟨{.lt, .eq, .gt}, by simp⟩, fun x => by cases x <;> simp⟩

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

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

Разделы

Аффилиация

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