isWellOrder

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.Lt.isWellOrder

English

The ordering on Fin n is a well order.

Русский

Упорядочивание на Fin(n) по отношению < является хорошоупорядоченным.

LaTeX

$$$\mathrm{IsWellOrder}(\mathrm{Fin}(n), <)$$$

Lean4

/-- The ordering on `Fin n` is a well order. -/
instance isWellOrder (n) : IsWellOrder (Fin n) (· < ·) :=
  (valOrderEmb n).isWellOrder

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

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

Разделы

Аффилиация

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