instIsEmptyOfIsWellOrder

Mathlib.Order.InitialSeg

URI: https://scilib.ai/kg/mathlib#PrincipalSeg.instIsEmptyOfIsWellOrder

English

If IsWellOrder α r, then there is no f : r ≺i r (i.e., no self-embedding as a principal segment).

Русский

Если α упорядочено по r, то не существует f : r ≺i r (нет самовложенного начального отрезка).

LaTeX

$$$\neg \exists f : r \prec i r$$$

Lean4

instance (r : α → α → Prop) [IsWellOrder α r] : IsEmpty (r ≺i r) :=
  ⟨fun f => f.irrefl⟩

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

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

Разделы

Аффилиация

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