instWellFoundedLT

Mathlib.SetTheory.Ordinal.NaturalOps

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

English

NatOrdinal is endowed with a well-founded less-than relation (WellFoundedLT).

Русский

NatOrdinal обладает хорошо упорядоченным отношением меньше (<) (WellFoundedLT).

LaTeX

$$$\\text{WellFoundedLT}(\\mathrm{NatOrdinal})$$$

Lean4

instance : WellFoundedLT NatOrdinal :=
  Ordinal.wellFoundedLT

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

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

Разделы

Аффилиация

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