Well-founded sets

A well-founded subset of an ordered type is one on which the relation < is well-founded.

Main Definitions

• Set.WellFoundedOn s r indicates that the relation r is well-founded when restricted to the set s.
• Set.IsWF s indicates that < is well-founded when restricted to s.
• Set.PartiallyWellOrderedOn s r indicates that the relation r is partially well-ordered (also known as well quasi-ordered) when restricted to the set s.
• Set.IsPWO s indicates that any infinite sequence of elements in s contains an infinite monotone subsequence. Note that this is equivalent to containing only two comparable elements.

Main Results

• Higman's Lemma, Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂, shows that if r is partially well-ordered on s, then List.SublistForall₂ is partially well-ordered on the set of lists of elements of s. The result was originally published by Higman, but this proof more closely follows Nash-Williams.
• Set.wellFoundedOn_iff relates well_founded_on to the well-foundedness of a relation on the original type, to avoid dealing with subtypes.
• Set.IsWF.mono shows that a subset of a well-founded subset is well-founded.
• Set.IsWF.union shows that the union of two well-founded subsets is well-founded.
• Finset.isWF shows that all Finsets are well-founded.

TODO

Prove that s is partial well ordered iff it has no infinite descending chain or antichain.

References

• Higman, Ordering by Divisibility in Abstract Algebras
• Nash-Williams, On Well-Quasi-Ordering Finite Trees

Relations well-founded on sets

def Set.WellFoundedOn {α : Type u_2} (s : Set α) (r : α → α → Prop) : Prop

s.WellFoundedOn r indicates that the relation r is well-founded when restricted to s.

Equations

• s.WellFoundedOn r = WellFounded fun (a b : ↑s) => r ↑a ↑b

@[simp]

theorem Set.wellFoundedOn_empty {α : Type u_2} (r : α → α → Prop) : ∅.WellFoundedOn r

theorem Set.wellFoundedOn_iff {α : Type u_2} {r : α → α → Prop} {s : Set α} : s.WellFoundedOn r ↔ WellFounded fun (a b : α) => r a b ∧ a ∈ s ∧ b ∈ s

@[simp]

theorem Set.wellFoundedOn_univ {α : Type u_2} {r : α → α → Prop} : Set.univ.WellFoundedOn r ↔ WellFounded r

theorem WellFounded.wellFoundedOn {α : Type u_2} {r : α → α → Prop} {s : Set α} : WellFounded r → s.WellFoundedOn r

@[simp]

theorem Set.wellFoundedOn_range {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} : (Set.range f).WellFoundedOn r ↔ WellFounded (r on f)

@[simp]

theorem Set.wellFoundedOn_image {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} {s : Set β} : (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

theorem Set.WellFoundedOn.induction {α : Type u_2} {r : α → α → Prop} {s : Set α} {x : α} (hs : s.WellFoundedOn r) (hx : x ∈ s) {P : α → Prop} (hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y) : P x

theorem Set.WellFoundedOn.mono {α : Type u_2} {r r' : α → α → Prop} {s t : Set α} (h : t.WellFoundedOn r') (hle : r ≤ r') (hst : s ⊆ t) : s.WellFoundedOn r

theorem Set.WellFoundedOn.mono' {α : Type u_2} {r r' : α → α → Prop} {s : Set α} (h : ∀ a ∈ s, ∀ b ∈ s, r' a b → r a b) : s.WellFoundedOn r → s.WellFoundedOn r'

theorem Set.WellFoundedOn.subset {α : Type u_2} {r : α → α → Prop} {s t : Set α} (h : t.WellFoundedOn r) (hst : s ⊆ t) : s.WellFoundedOn r

theorem Set.WellFoundedOn.acc_iff_wellFoundedOn {α : Type u_6} {r : α → α → Prop} {a : α} : [Acc r a, {b : α | Relation.ReflTransGen r b a}.WellFoundedOn r, {b : α | Relation.TransGen r b a}.WellFoundedOn r].TFAE

a is accessible under the relation r iff r is well-founded on the downward transitive closure of a under r (including a or not).

instance Set.IsStrictOrder.subset {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} : IsStrictOrder α fun (a b : α) => r a b ∧ a ∈ s ∧ b ∈ s

theorem Set.wellFoundedOn_iff_no_descending_seq {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} : s.WellFoundedOn r ↔ ∀ (f : (fun (x1 x2 : ℕ) => x1 > x2) ↪r r), ¬∀ (n : ℕ), f n ∈ s

theorem Set.WellFoundedOn.union {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s t : Set α} (hs : s.WellFoundedOn r) (ht : t.WellFoundedOn r) : (s ∪ t).WellFoundedOn r

@[simp]

theorem Set.wellFoundedOn_union {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s t : Set α} : (s ∪ t).WellFoundedOn r ↔ s.WellFoundedOn r ∧ t.WellFoundedOn r

Sets well-founded w.r.t. the strict inequality

def Set.IsWF {α : Type u_2} [LT α] (s : Set α) : Prop

s.IsWF indicates that < is well-founded when restricted to s.

Equations

• s.IsWF = s.WellFoundedOn fun (x1 x2 : α) => x1 < x2

@[simp]

theorem Set.isWF_empty {α : Type u_2} [LT α] : ∅.IsWF

theorem Set.isWF_univ_iff {α : Type u_2} [LT α] : Set.univ.IsWF ↔ WellFounded fun (x1 x2 : α) => x1 < x2

theorem Set.IsWF.mono {α : Type u_2} [LT α] {s t : Set α} (h : t.IsWF) (st : s ⊆ t) : s.IsWF

theorem Set.IsWF.union {α : Type u_2} [Preorder α] {s t : Set α} (hs : s.IsWF) (ht : t.IsWF) : (s ∪ t).IsWF

@[simp]

theorem Set.isWF_union {α : Type u_2} [Preorder α] {s t : Set α} : (s ∪ t).IsWF ↔ s.IsWF ∧ t.IsWF

theorem Set.isWF_iff_no_descending_seq {α : Type u_2} [Preorder α] {s : Set α} : s.IsWF ↔ ∀ (f : ℕ → α), StrictAnti f → ¬∀ (n : ℕ), f (OrderDual.toDual n) ∈ s

Partially well-ordered sets

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.

def Set.PartiallyWellOrderedOn {α : Type u_2} (s : Set α) (r : α → α → Prop) : Prop

A subset 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.

Equations

• s.PartiallyWellOrderedOn r = ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

theorem Set.PartiallyWellOrderedOn.mono {α : Type u_2} {r : α → α → Prop} {s t : Set α} (ht : t.PartiallyWellOrderedOn r) (h : s ⊆ t) : s.PartiallyWellOrderedOn r

@[simp]

theorem Set.partiallyWellOrderedOn_empty {α : Type u_2} (r : α → α → Prop) : ∅.PartiallyWellOrderedOn r

theorem Set.PartiallyWellOrderedOn.union {α : Type u_2} {r : α → α → Prop} {s t : Set α} (hs : s.PartiallyWellOrderedOn r) (ht : t.PartiallyWellOrderedOn r) : (s ∪ t).PartiallyWellOrderedOn r

@[simp]

theorem Set.partiallyWellOrderedOn_union {α : Type u_2} {r : α → α → Prop} {s t : Set α} : (s ∪ t).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r ∧ t.PartiallyWellOrderedOn r

theorem Set.PartiallyWellOrderedOn.image_of_monotone_on {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {f : α → β} {s : Set α} (hs : s.PartiallyWellOrderedOn r) (hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) : (f '' s).PartiallyWellOrderedOn r'

theorem IsAntichain.finite_of_partiallyWellOrderedOn {α : Type u_2} {r : α → α → Prop} {s : Set α} (ha : IsAntichain r s) (hp : s.PartiallyWellOrderedOn r) : s.Finite

theorem Set.Finite.partiallyWellOrderedOn {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] (hs : s.Finite) : s.PartiallyWellOrderedOn r

theorem IsAntichain.partiallyWellOrderedOn_iff {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] (hs : IsAntichain r s) : s.PartiallyWellOrderedOn r ↔ s.Finite

@[simp]

theorem Set.partiallyWellOrderedOn_singleton {α : Type u_2} {r : α → α → Prop} [IsRefl α r] (a : α) : {a}.PartiallyWellOrderedOn r

theorem Set.Subsingleton.partiallyWellOrderedOn {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] (hs : s.Subsingleton) : s.PartiallyWellOrderedOn r

@[simp]

theorem Set.partiallyWellOrderedOn_insert {α : Type u_2} {r : α → α → Prop} {s : Set α} {a : α} [IsRefl α r] : (insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r

theorem Set.PartiallyWellOrderedOn.insert {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] (h : s.PartiallyWellOrderedOn r) (a : α) : (insert a s).PartiallyWellOrderedOn r

theorem Set.partiallyWellOrderedOn_iff_finite_antichains {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] [IsSymm α r] : s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] [IsTrans α r] (h : s.PartiallyWellOrderedOn r) (f : ℕ → α) (hf : ∀ (n : ℕ), f n ∈ s) : ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

theorem Set.partiallyWellOrderedOn_iff_exists_monotone_subseq {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsRefl α r] [IsTrans α r] : s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))

theorem Set.PartiallyWellOrderedOn.prod {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α} [IsRefl α r] [IsTrans α r] {t : Set β} (hs : s.PartiallyWellOrderedOn r) (ht : t.PartiallyWellOrderedOn r') : (s ×ˢ t).PartiallyWellOrderedOn fun (x y : α × β) => r x.1 y.1 ∧ r' x.2 y.2

theorem Set.PartiallyWellOrderedOn.wellFoundedOn {α : Type u_2} {r : α → α → Prop} {s : Set α} [IsPreorder α r] (h : s.PartiallyWellOrderedOn r) : s.WellFoundedOn fun (a b : α) => r a b ∧ ¬r b a

def Set.IsPWO {α : Type u_2} [Preorder α] (s : Set α) : Prop

A subset of a preorder is partially well-ordered when any infinite sequence contains a monotone subsequence of length 2 (or equivalently, an infinite monotone subsequence).

Equations

• s.IsPWO = s.PartiallyWellOrderedOn fun (x1 x2 : α) => x1 ≤ x2

theorem Set.IsPWO.mono {α : Type u_2} [Preorder α] {s t : Set α} (ht : t.IsPWO) : s ⊆ t → s.IsPWO

theorem Set.IsPWO.exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) (f : ℕ → α) (hf : ∀ (n : ℕ), f n ∈ s) : ∃ (g : ℕ ↪o ℕ), Monotone (f ∘ ⇑g)

theorem Set.isPWO_iff_exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} : s.IsPWO ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), Monotone (f ∘ ⇑g)

theorem Set.IsPWO.isWF {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) : s.IsWF

theorem Set.IsPWO.prod {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.IsPWO) (ht : t.IsPWO) : (s ×ˢ t).IsPWO

theorem Set.IsPWO.image_of_monotoneOn {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : s.IsPWO) {f : α → β} (hf : MonotoneOn f s) : (f '' s).IsPWO

theorem Set.IsPWO.image_of_monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : s.IsPWO) {f : α → β} (hf : Monotone f) : (f '' s).IsPWO

theorem Set.IsPWO.union {α : Type u_2} [Preorder α] {s t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) : (s ∪ t).IsPWO

@[simp]

theorem Set.isPWO_union {α : Type u_2} [Preorder α] {s t : Set α} : (s ∪ t).IsPWO ↔ s.IsPWO ∧ t.IsPWO

theorem Set.Finite.isPWO {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Finite) : s.IsPWO

@[simp]

theorem Set.isPWO_of_finite {α : Type u_2} [Preorder α] {s : Set α} [Finite α] : s.IsPWO

@[simp]

theorem Set.isPWO_singleton {α : Type u_2} [Preorder α] (a : α) : {a}.IsPWO

@[simp]

theorem Set.isPWO_empty {α : Type u_2} [Preorder α] : ∅.IsPWO

theorem Set.Subsingleton.isPWO {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Subsingleton) : s.IsPWO

@[simp]

theorem Set.isPWO_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} : (insert a s).IsPWO ↔ s.IsPWO

theorem Set.IsPWO.insert {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) (a : α) : (insert a s).IsPWO

theorem Set.Finite.isWF {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Finite) : s.IsWF

@[simp]

theorem Set.isWF_singleton {α : Type u_2} [Preorder α] {a : α} : {a}.IsWF

theorem Set.Subsingleton.isWF {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Subsingleton) : s.IsWF

@[simp]

theorem Set.isWF_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} : (insert a s).IsWF ↔ s.IsWF

theorem Set.IsWF.insert {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsWF) (a : α) : (insert a s).IsWF

theorem Set.Finite.wellFoundedOn {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} (hs : s.Finite) : s.WellFoundedOn r

@[simp]

theorem Set.wellFoundedOn_singleton {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {a : α} : {a}.WellFoundedOn r

theorem Set.Subsingleton.wellFoundedOn {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} (hs : s.Subsingleton) : s.WellFoundedOn r

@[simp]

theorem Set.wellFoundedOn_insert {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} {a : α} : (insert a s).WellFoundedOn r ↔ s.WellFoundedOn r

@[simp]

theorem Set.wellFoundedOn_sdiff_singleton {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} {a : α} : (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r

theorem Set.WellFoundedOn.insert {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} (h : s.WellFoundedOn r) (a : α) : (insert a s).WellFoundedOn r

theorem Set.WellFoundedOn.sdiff_singleton {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] {s : Set α} (h : s.WellFoundedOn r) (a : α) : (s \ {a}).WellFoundedOn r

theorem Set.WellFoundedOn.mapsTo {α : Type u_6} {β : Type u_7} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β} (h : Set.MapsTo f t s) (hw : s.WellFoundedOn r) : t.WellFoundedOn (r on f)

theorem Set.IsWF.isPWO {α : Type u_2} [LinearOrder α] {s : Set α} (hs : s.IsWF) : s.IsPWO

theorem Set.isWF_iff_isPWO {α : Type u_2} [LinearOrder α] {s : Set α} : s.IsWF ↔ s.IsPWO

In a linear order, the predicates Set.IsWF and Set.IsPWO are equivalent.

@[simp]

theorem Finset.partiallyWellOrderedOn {α : Type u_2} {r : α → α → Prop} [IsRefl α r] (s : Finset α) : (↑s).PartiallyWellOrderedOn r

@[simp]

theorem Finset.isPWO {α : Type u_2} [Preorder α] (s : Finset α) : (↑s).IsPWO

@[simp]

theorem Finset.isWF {α : Type u_2} [Preorder α] (s : Finset α) : (↑s).IsWF

@[simp]

theorem Finset.wellFoundedOn {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset α) : (↑s).WellFoundedOn r

theorem Finset.wellFoundedOn_sup {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

theorem Finset.partiallyWellOrderedOn_sup {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : Finset ι) {f : ι → Set α} : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

theorem Finset.isWF_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (s.sup f).IsWF ↔ ∀ i ∈ s, (f i).IsWF

theorem Finset.isPWO_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO

@[simp]

theorem Finset.wellFoundedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [IsStrictOrder α r] (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

@[simp]

theorem Finset.partiallyWellOrderedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

@[simp]

theorem Finset.isWF_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).IsWF ↔ ∀ i ∈ s, (f i).IsWF

@[simp]

theorem Finset.isPWO_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ι → Set α} : (⋃ i ∈ s, f i).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO

noncomputable def Set.IsWF.min {α : Type u_2} [Preorder α] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty) : α

Set.IsWF.min returns a minimal element of a nonempty well-founded set.

Equations

• hs.min hn = ↑(WellFounded.min hs Set.univ ⋯)

theorem Set.IsWF.min_mem {α : Type u_2} [Preorder α] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty) : hs.min hn ∈ s

theorem Set.IsWF.not_lt_min {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) (ha : a ∈ s) : ¬a < hs.min hn

theorem Set.IsWF.min_of_subset_not_lt_min {α : Type u_2} [Preorder α] {s t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s ⊆ t) : ¬hs.min hsn < ht.min htn

@[simp]

theorem Set.isWF_min_singleton {α : Type u_2} [Preorder α] (a : α) {hs : {a}.IsWF} {hn : {a}.Nonempty} : hs.min hn = a

theorem Set.IsWF.min_eq_of_lt {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (ha : a ∈ s) (hlt : ∀ b ∈ s, b ≠ a → a < b) : hs.min ⋯ = a

theorem Set.IsWF.min_eq_of_le {α : Type u_2} [PartialOrder α] {s : Set α} {a : α} (hs : s.IsWF) (ha : a ∈ s) (hle : ∀ b ∈ s, a ≤ b) : hs.min ⋯ = a

theorem Set.IsWF.min_le {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) (ha : a ∈ s) : hs.min hn ≤ a

theorem Set.IsWF.le_min_iff {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) : a ≤ hs.min hn ↔ ∀ b ∈ s, a ≤ b

theorem Set.IsWF.min_le_min_of_subset {α : Type u_2} [LinearOrder α] {s t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s ⊆ t) : ht.min htn ≤ hs.min hsn

theorem Set.IsWF.min_union {α : Type u_2} [LinearOrder α] {s t : Set α} (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty) : ⋯.min ⋯ = hs.min hsn ⊓ ht.min htn

theorem BddBelow.wellFoundedOn_lt {α : Type u_2} {s : Set α} [Preorder α] [LocallyFiniteOrder α] : BddBelow s → s.WellFoundedOn fun (x1 x2 : α) => x1 < x2

theorem BddAbove.wellFoundedOn_gt {α : Type u_2} {s : Set α} [Preorder α] [LocallyFiniteOrder α] : BddAbove s → s.WellFoundedOn fun (x1 x2 : α) => x1 > x2

def Set.PartiallyWellOrderedOn.IsBadSeq {α : Type u_2} (r : α → α → Prop) (s : Set α) (f : ℕ → α) : Prop

In the context of partial well-orderings, a bad sequence is a nonincreasing sequence whose range is contained in a particular set s. One exists if and only if s is not partially well-ordered.

Equations

• Set.PartiallyWellOrderedOn.IsBadSeq r s f = ((∀ (n : ℕ), f n ∈ s) ∧ ∀ (m n : ℕ), m < n → ¬r (f m) (f n))

theorem Set.PartiallyWellOrderedOn.iff_forall_not_isBadSeq {α : Type u_2} (r : α → α → Prop) (s : Set α) : s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬Set.PartiallyWellOrderedOn.IsBadSeq r s f

def Set.PartiallyWellOrderedOn.IsMinBadSeq {α : Type u_2} (r : α → α → Prop) (rk : α → ℕ) (s : Set α) (n : ℕ) (f : ℕ → α) : Prop

This indicates that every bad sequence g that agrees with f on the first n terms has rk (f n) ≤ rk (g n).

Equations

• Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f = ∀ (g : ℕ → α), (∀ m < n, f m = g m) → rk (g n) < rk (f n) → ¬Set.PartiallyWellOrderedOn.IsBadSeq r s g

noncomputable def Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq {α : Type u_2} (r : α → α → Prop) (rk : α → ℕ) (s : Set α) (n : ℕ) (f : ℕ → α) (hf : Set.PartiallyWellOrderedOn.IsBadSeq r s f) : { g : ℕ → α // (∀ m < n, f m = g m) ∧ Set.PartiallyWellOrderedOn.IsBadSeq r s g ∧ Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n g }

Given a bad sequence f, this constructs a bad sequence that agrees with f on the first n terms and is minimal at n.

Equations

• One or more equations did not get rendered due to their size.

theorem Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad {α : Type u_2} (r : α → α → Prop) (rk : α → ℕ) (s : Set α) : (∃ (f : ℕ → α), Set.PartiallyWellOrderedOn.IsBadSeq r s f) → ∃ (f : ℕ → α), Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f

theorem Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq {α : Type u_2} {r : α → α → Prop} (rk : α → ℕ) {s : Set α} : s.PartiallyWellOrderedOn r ↔ ¬∃ (f : ℕ → α), Set.PartiallyWellOrderedOn.IsBadSeq r s f ∧ ∀ (n : ℕ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f

theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ {α : Type u_2} (r : α → α → Prop) [IsRefl α r] [IsTrans α r] {s : Set α} (h : s.PartiallyWellOrderedOn r) : {l : List α | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Higman's Lemma, which states that for any reflexive, transitive relation r which is partially well-ordered on a set s, the relation List.SublistForall₂ r is partially well-ordered on the set of lists of elements of s. That relation is defined so that List.SublistForall₂ r l₁ l₂ whenever l₁ related pointwise by r to a sublist of l₂.

theorem Set.PartiallyWellOrderedOn.subsetProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hα : ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO) (hβ : ∀ (a : α), {y : β | toLex (a, y) ∈ s}.IsPWO) : s.IsPWO

theorem Set.PartiallyWellOrderedOn.imageProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) : ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO

theorem Set.PartiallyWellOrderedOn.fiberProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) (a : α) : {y : β | toLex (a, y) ∈ s}.IsPWO

theorem Set.PartiallyWellOrderedOn.ProdLex_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} : s.IsPWO ↔ ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO ∧ ∀ (a : α), {y : β | toLex (a, y) ∈ s}.IsPWO

theorem WellFounded.isWF {α : Type u_2} [LT α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) (s : Set α) : s.IsWF

theorem Pi.isPWO {ι : Type u_1} {α : ι → Type u_6} [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsWellOrder (α i) fun (x1 x2 : α i) => x1 < x2] [Finite ι] (s : Set ((i : ι) → α i)) : s.IsPWO

A version of Dickson's lemma any subset of functions Π s : σ, α s is partially well ordered, when σ is a Fintype and each α s is a linear well order. This includes the classical case of Dickson's lemma that ℕ ^ n is a well partial order. Some generalizations would be possible based on this proof, to include cases where the target is partially well ordered, and also to consider the case of Set.PartiallyWellOrderedOn instead of Set.IsPWO.

theorem WellFounded.prod_lex_of_wellFoundedOn_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β} (hα : WellFounded (rα on f)) (hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)) : WellFounded (Prod.Lex rα rβ on fun (c : γ) => (f c, g c))

Stronger version of WellFounded.prod_lex. Instead of requiring rβ on g to be well-founded, we only require it to be well-founded on fibers of f.

theorem Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β} {s : Set γ} (hα : s.WellFoundedOn (rα on f)) (hβ : ∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (rβ on g)) : s.WellFoundedOn (Prod.Lex rα rβ on fun (c : γ) => (f c, g c))

theorem WellFounded.sigma_lex_of_wellFoundedOn_fiber {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι} {g : (i : ι) → γ → π i} (hι : WellFounded (rι on f)) (hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)) : WellFounded (Sigma.Lex rι rπ on fun (c : γ) => ⟨f c, g (f c) c⟩)

Stronger version of PSigma.lex_wf. Instead of requiring rπ on g to be well-founded, we only require it to be well-founded on fibers of f.

theorem Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι} {g : (i : ι) → γ → π i} {s : Set γ} (hι : s.WellFoundedOn (rι on f)) (hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)) : s.WellFoundedOn (Sigma.Lex rι rπ on fun (c : γ) => ⟨f c, g (f c) c⟩)