wellQuasiOrderedLE_iff_wellFoundedLT

English

A linear WellQuasiOrderedLE is the same as a well-ordered set in the strict sense: WellQuasiOrderedLE α ⇔ WellFoundedLT α.

Русский

Для линейного порядка WQO LE эквивалентно хорошо основанному строгому порядку: WQO LE эквивалентно WellFoundedLT.

LaTeX

$$$\\mathrm{WellQuasiOrderedLE}(\\alpha) \\iff \\mathrm{WellFoundedLT}(\\alpha)$$$

Lean4

/-- A linear WQO is the same thing as a well-order. -/
theorem wellQuasiOrderedLE_iff_wellFoundedLT : WellQuasiOrderedLE α ↔ WellFoundedLT α :=
  by
  rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]
  exact fun _ s hs ↦ hs.subsingleton.finite

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