Theorems · Theorem · order theory

Set.IsPWO.of_linearOrder

∀ {α : Type u_2} [inst : LinearOrder α] [WellFoundedLT α] (s : Set α), s.IsPWO

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.

Defined in

Mathlib.Order.WellFoundedSet

Cited by

0 results in Mathlib

Foundations

Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderWellFoundedLT