instWellFoundedLT

Mathlib.Data.Nat.PartENat

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

English

There is an instance of WellFoundedLT for PartENat, i.e., LT is well-founded.

Русский

Существует инстанс WellFoundedLT для PartENat, то есть LT хорошо упорядочено.

LaTeX

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

Lean4

instance : WellFoundedLT PartENat :=
  ⟨lt_wf⟩

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

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

Разделы

Аффилиация

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