Theorems · Definition · order theory
Set.PartiallyWellOrderedOn
{α : Type u_2} → Set α → (α → α → Prop) → Props.PartiallyWellOrderedOn r indicates that the relation r is WellQuasiOrdered when
restricted to s.
A set is partially well-ordered by a relation r when any infinite sequence contains two elements
where the first is related to the second by r. Equivalently, any antichain (see IsAntichain) is
finite, see Set.partiallyWellOrderedOn_iff_finite_antichains.
TODO: rename this to WellQuasiOrderedOn to match WellQuasiOrdered.
- Defined in
- Mathlib.Order.WellFoundedSet
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Subrelproof · cited by 53
- WellQuasiOrderedproof · cited by 15
Cited by35
Results whose statement or proof uses this declaration.
- Set.IsPWOproof · cited by 99
- Set.VAddAntidiagonal.finite_of_isPWOproof · cited by 16
- Set.PartiallyWellOrderedOn.exists_monotone_subseqstatement and proof · cited by 9
- IsAntichain.finite_of_partiallyWellOrderedOnstatement and proof · cited by 6
- Set.partiallyWellOrderedOn_iff_exists_ltstatement · cited by 6
- Set.Finite.partiallyWellOrderedOnstatement · cited by 5
- Set.PartiallyWellOrderedOn.image_of_monotone_onstatement and proof · cited by 4
- Set.PartiallyWellOrderedOn.monostatement and proof · cited by 4
- Set.PartiallyWellOrderedOn.exists_ltstatement and proof · cited by 3
- Set.PartiallyWellOrderedOn.wellFoundedOnstatement and proof · cited by 3
- Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂statement and proof · cited by 2
- Set.PartiallyWellOrderedOn.unionstatement and proof · cited by 2