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

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.IsPWO.exists_le_minimal {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.IsPWO) (ha : a ∈ s) :

∃ b ≤ a, Minimal (fun (x : α) => x ∈ s) b

theorem Set.IsPWO.exists_minimal {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) (hs : s.Nonempty) :

∃ (a : α), Minimal (fun (x : α) => x ∈ s) a

theorem Set.IsPWO.exists_minimalFor {ι : Type u_1} {α : Type u_2} [Preorder α] (f : ι → α) (s : Set ι) (h : (f '' s).IsPWO) (hs : s.Nonempty) :

∃ (i : ι), MinimalFor (fun (x : ι) => x ∈ s) f i

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.

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.