to_wellFoundedLT — Mathlib

English

Every finite type can be endowed with a well-founded linear order.

Русский

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

LaTeX

$$$\exists \le \; (\text{LinearOrder}(\alpha)) \wedge \mathrm{WellFounded}(\alpha, \le)$$$

Lean4

instance (priority := 100) to_wellFoundedLT [Preorder α] : WellFoundedLT α :=
  ⟨wellFounded_of_trans_of_irrefl _⟩
    -- See note [lower instance priority]

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