Documentation

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

s.WellFoundedOn r indicates that the relation r is WellFounded when restricted to s.

Equations

s.WellFoundedOn r = WellFounded (Subrel r fun (x : α) => x ∈ s)

Instances For

@[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} :

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 : β → α} :

(range f).WellFoundedOn r ↔ WellFounded (Function.onFun r f)

@[simp]

theorem Set.wellFoundedOn_image {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} {s : Set β} :

(f '' s).WellFoundedOn r ↔ s.WellFoundedOn (Function.onFun r 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) :

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) :

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 α) :

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

Equations

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

Instances For

@[simp]

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

∅.IsWF

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

s.IsWF

theorem Set.isWF_univ_iff {α : Type u_2} [LT α] :

univ.IsWF ↔ WellFoundedLT α

theorem Set.IsWF.of_wellFoundedLT {α : Type u_2} [LT α] [h : WellFoundedLT α] (s : Set α) :

s.IsWF

@[deprecated Set.IsWF.of_wellFoundedLT (since := "2025-01-16")]

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

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 n ∈ s

Partially well-ordered sets #

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

s.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.

Equations

s.PartiallyWellOrderedOn r = WellQuasiOrdered (Subrel r fun (x : α) => x ∈ s)

Instances For

theorem Set.PartiallyWellOrderedOn.exists_lt {α : Type u_2} {r : α → α → Prop} {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ (n : ℕ), f n ∈ s) :

∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

theorem Set.partiallyWellOrderedOn_iff_exists_lt {α : Type u_2} {r : α → α → Prop} {s : Set α} :

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 α} [IsPreorder α 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 α} [IsPreorder α 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 α} [IsPreorder α 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 α) :

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

Instances For

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) :

@[simp]

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

@[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) :

@[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) :

@[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) :

@[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 : MapsTo f t s) (hw : s.WellFoundedOn r) :

t.WellFoundedOn (Function.onFun r f)

theorem Set.isPWO_iff_isWF {α : Type u_2} [LinearOrder α] {s : Set α} :

s.IsPWO ↔ s.IsWF

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

theorem Set.IsWF.isPWO {α : Type u_2} [LinearOrder α] {s : Set α} :

s.IsWF → s.IsPWO

Alias of the reverse direction of Set.isPWO_iff_isWF.

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

@[deprecated Set.isPWO_iff_isWF (since := "2025-01-21")]

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

s.IsWF ↔ s.IsPWO

theorem Set.IsPWO.of_linearOrder {α : Type u_2} [LinearOrder α] [WellFoundedLT α] (s : Set α) :

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.

@[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 ⋯)

Instances For

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 ⋯ = Min.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

theorem BddBelow.isWF {α : Type u_2} {s : Set α} [Preorder α] [LocallyFiniteOrder α] :

BddBelow s → s.IsWF

theorem Set.PartiallyWellOrderedOn.bddAbove_preimage {α : Type u_2} {r : α → α → Prop} {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)) :

BddAbove (f ⁻¹' s)

theorem Set.PartiallyWellOrderedOn.exists_notMem_of_gt {α : Type u_2} {r : α → α → Prop} {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)) :

∃ (k : ℕ), ∀ (m : ℕ), k < m → f m ∉ s

@[deprecated Set.PartiallyWellOrderedOn.exists_notMem_of_gt (since := "2025-05-23")]

theorem Set.PartiallyWellOrderedOn.exists_not_mem_of_gt {α : Type u_2} {r : α → α → Prop} {s : Set α} (hs : s.PartiallyWellOrderedOn r) {f : ℕ → α} (hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)) :

∃ (k : ℕ), ∀ (m : ℕ), k < m → f m ∉ s

Alias of Set.PartiallyWellOrderedOn.exists_notMem_of_gt.

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

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))

Instances For

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

s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f

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

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

Instances For

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

{ g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ 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.

Instances For

theorem Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad {α : Type u_2} (r : α → α → Prop) (rk : α → ℕ) (s : Set α) :

(∃ (f : ℕ → α), IsBadSeq r s f) → ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), 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 : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ {α : Type u_2} (r : α → α → Prop) [IsPreorder α 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) :

theorem Set.PartiallyWellOrderedOn.imageProdLex {α : Type u_2} {β : Type u_3} [Preorder α] [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} [Preorder α] [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 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)) :

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 (Function.onFun rα f)) (hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) :

WellFounded (Function.onFun (Prod.Lex rα rβ) 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 (Function.onFun rα f)) (hβ : ∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) :

s.WellFoundedOn (Function.onFun (Prod.Lex rα rβ) 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 (Function.onFun rι f)) (hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (Function.onFun (rπ i) (g i))) :

WellFounded (Function.onFun (Sigma.Lex rι rπ) 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.