lt_wf

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.lt_wf

English

The relation < on NatOrdinal is well-founded.

Русский

Отношение < на NatOrdinal является хорошо упорядоченным (well-founded).

LaTeX

$$$\\mathrm{WellFounded}(<) \\text{ on } \\mathrm{NatOrdinal}$$$

Lean4

theorem lt_wf : @WellFounded NatOrdinal (· < ·) :=
  Ordinal.lt_wf

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

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

Разделы

Аффилиация

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