isWellOrder_lt — Mathlib

English

Let α be a type with a linear order and WellFoundedLT α. Then the less-than relation is a well-order on α.

Русский

Пусть α — множество с линейным порядком и WellFoundedLT α. Тогда отношение ≤ (меньше) образует хорошо упорядоченный порядок на α.

LaTeX

$$$\operatorname{IsWellOrder}(\alpha, <)$$$

Lean4

instance (priority := 100) isWellOrder_lt [LinearOrder α] [WellFoundedLT α] : IsWellOrder α (· < ·) where

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