of_linearOrder — Mathlib

English

If α is a linear order and < on α is well-founded, then every subset s ⊆ α is partially well-ordered under ≤.

Русский

Если α образует линейный порядок и < на α хорошо основано, то любое множество s ⊆ α частично хорошо упорядовано по ≤.

LaTeX

$$$[WellFoundedLT\\,\\alpha] \\; \\Rightarrow \\; s.IsPWO$$$

Lean4

/-- If `α` is a linear order with well-founded `<`, then any set in it is a partially well-ordered set.
Note this does not hold without the linearity assumption.
-/
theorem of_linearOrder [WellFoundedLT α] (s : Set α) : s.IsPWO :=
  (IsWF.of_wellFoundedLT s).isPWO

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