isPWO_iff_isWF — Mathlib

English

In a linear order, a set is partially well-ordered under ≤ if and only if it is well-founded under <.

Русский

В линейном порядке множество частично хорошо упорядовано по ≤ тогда и только тогда, когда оно хорошо упорядовано по <.

LaTeX

$$$ s.IsPWO \\iff s.IsWF $$$

Lean4

/-- In a linear order, the predicates `Set.IsPWO` and `Set.IsWF` are equivalent. -/
theorem isPWO_iff_isWF : s.IsPWO ↔ s.IsWF :=
  by
  change WellQuasiOrdered (· ≤ ·) ↔ WellFounded (· < ·)
  rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]

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