wellFounded_lt — Mathlib

English

If α is a type with a strict order < and WellFoundedLT, then < is a well-founded relation on α.

Русский

Пусть у типа α есть строгие отношения < и свойство WellFoundedLT. Тогда < является хорошо основанным отношением на α.

LaTeX

$$$\\mathrm{WellFounded}(<)$ на $\\alpha\$$$

Lean4

theorem wellFounded_lt [LT α] [WellFoundedLT α] : @WellFounded α (· < ·) :=
  IsWellFounded.wf

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