wellFoundedLT

Mathlib.Data.DFinsupp.WellFounded

URI: https://scilib.ai/kg/mathlib#Function.wellFoundedLT

English

Under a trichotomy assumption on r and a well-founded swap, the Lex order is well-founded.

Русский

При трёхчётности r и хорошо основанном swap, Lex хорошо основан.

LaTeX

$$$\\mathrm{wellFounded'}(DFinsupp.Lex(r,s))$$$

Lean4

instance wellFoundedLT {α} [Finite ι] [Preorder α] [WellFoundedLT α] : WellFoundedLT (ι → α) :=
  Pi.wellFoundedLT

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

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

Разделы

Аффилиация

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