to_wellFoundedGT

Mathlib.Data.Fintype.Card

URI: https://scilib.ai/kg/mathlib#Finite.to_wellFoundedGT

English

Every finite type can be endowed with a well-founded GT (greater-than) order.

Русский

Каждому конечному типу можно придать хорошо основанный порядок GT (по возрастанию).

LaTeX

$$$\exists \ge \; (\text{LinearOrder}(\alpha)) \wedge \mathrm{WellFounded}(\alpha, \ge)$$$

Lean4

instance (priority := 100) to_wellFoundedGT [Preorder α] : WellFoundedGT α :=
  ⟨wellFounded_of_trans_of_irrefl _⟩

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

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

Разделы

Аффилиация

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