mathlib documentation

order.well_founded_set

Well-founded sets #

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

Main Definitions #

Definitions for Hahn Series #

Main Results #

References #

def set.well_founded_on {α : Type u_1} (s : set α) (r : α → α → Prop) :
Prop

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

Equations
theorem set.well_founded_on_iff {α : Type u_1} {s : set α} {r : α → α → Prop} :
s.well_founded_on r well_founded (λ (a b : α), r a b a s b s)
theorem set.well_founded_on.induction {α : Type u_1} {s : set α} {r : α → α → Prop} (hs : s.well_founded_on r) {x : α} (hx : x s) {P : α → Prop} (hP : ∀ (y : α), y s(∀ (z : α), z sr z yP z)P y) :
P x
@[instance]
def set.is_strict_order.subset {α : Type u_1} {s : set α} {r : α → α → Prop} [is_strict_order α r] :
is_strict_order α (λ (a b : α), r a b a s b s)
theorem set.well_founded_on_iff_no_descending_seq {α : Type u_1} {s : set α} {r : α → α → Prop} [is_strict_order α r] :
def set.is_wf {α : Type u_1} [has_lt α] (s : set α) :
Prop

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

Equations
theorem set.is_wf.mono {α : Type u_1} [has_lt α] {s t : set α} (h : t.is_wf) (st : s t) :
theorem set.is_wf_iff_no_descending_seq {α : Type u_1} [partial_order α] {s : set α} :
theorem set.is_wf.union {α : Type u_1} [partial_order α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s t).is_wf
def set.partially_well_ordered_on {α : Type u_1} (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
def set.is_pwo {α : Type u_1} [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
theorem set.partially_well_ordered_on.mono {α : Type u_1} {s t : set α} {r : α → α → Prop} (ht : t.partially_well_ordered_on r) (hsub : s t) :
theorem set.partially_well_ordered_on.image_of_monotone_on {α : Type u_1} {s : set α} {r : α → α → Prop} {β : Type u_2} {r' : β → β → Prop} (hs : s.partially_well_ordered_on r) {f : α → β} (hf : ∀ (a1 a2 : α), a1 sa2 sr a1 a2r' (f a1) (f a2)) :
theorem set.partially_well_ordered_on.exists_monotone_subseq {α : Type u_1} {s : set α} {r : α → α → Prop} [is_refl α r] [is_trans α r] (h : s.partially_well_ordered_on r) (f : → α) (hf : set.range f s) :
∃ (g : ↪o ), ∀ (m n : ), m nr (f (g m)) (f (g n))
theorem set.partially_well_ordered_on_iff_exists_monotone_subseq {α : Type u_1} {s : set α} {r : α → α → Prop} [is_refl α r] [is_trans α r] :
s.partially_well_ordered_on r ∀ (f : → α), set.range f s(∃ (g : ↪o ), ∀ (m n : ), m nr (f (g m)) (f (g n)))
theorem set.partially_well_ordered_on.well_founded_on {α : Type u_1} {s : set α} {r : α → α → Prop} [is_partial_order α r] (h : s.partially_well_ordered_on r) :
s.well_founded_on (λ (a b : α), r a b a b)
theorem set.is_pwo.is_wf {α : Type u_1} {s : set α} [partial_order α] (h : s.is_pwo) :
theorem set.is_pwo.exists_monotone_subseq {α : Type u_1} {s : set α} [partial_order α] (h : s.is_pwo) (f : → α) (hf : set.range f s) :
∃ (g : ↪o ), monotone (f g)
theorem set.is_pwo_iff_exists_monotone_subseq {α : Type u_1} {s : set α} [partial_order α] :
s.is_pwo ∀ (f : → α), set.range f s(∃ (g : ↪o ), monotone (f g))
theorem set.is_pwo.prod {α : Type u_1} {s t : set α} [partial_order α] (hs : s.is_pwo) (ht : t.is_pwo) :
(s.prod t).is_pwo
theorem set.is_pwo.image_of_monotone {α : Type u_1} {s : set α} [partial_order α] {β : Type u_2} [partial_order β] (hs : s.is_pwo) {f : α → β} (hf : monotone f) :
(f '' s).is_pwo
theorem set.is_pwo.union {α : Type u_1} {s t : set α} [partial_order α] (hs : s.is_pwo) (ht : t.is_pwo) :
(s t).is_pwo
theorem set.is_wf.is_pwo {α : Type u_1} [linear_order α] {s : set α} (hs : s.is_wf) :
theorem set.is_wf_iff_is_pwo {α : Type u_1} [linear_order α] {s : set α} :
@[simp]
theorem finset.partially_well_ordered_on {α : Type u_1} {r : α → α → Prop} [is_refl α r] (f : finset α) :
@[simp]
theorem finset.is_pwo {α : Type u_1} [partial_order α] (f : finset α) :
@[simp]
theorem finset.well_founded_on {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : finset α) :
@[simp]
theorem finset.is_wf {α : Type u_1} [partial_order α] (f : finset α) :
theorem set.finite.is_pwo {α : Type u_1} [partial_order α] {s : set α} (h : s.finite) :
@[simp]
theorem set.fintype.is_pwo {α : Type u_1} [partial_order α] {s : set α} [fintype α] :
@[simp]
theorem set.is_pwo_empty {α : Type u_1} [partial_order α] :
@[simp]
theorem set.is_pwo_singleton {α : Type u_1} [partial_order α] (a : α) :
{a}.is_pwo
theorem set.is_pwo.insert {α : Type u_1} [partial_order α] {s : set α} (a : α) (hs : s.is_pwo) :
def set.is_wf.min {α : Type u_1} [partial_order α] {s : set α} (hs : s.is_wf) (hn : s.nonempty) :
α

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

Equations
theorem set.is_wf.min_mem {α : Type u_1} [partial_order α] {s : set α} (hs : s.is_wf) (hn : s.nonempty) :
hs.min hn s
theorem set.is_wf.not_lt_min {α : Type u_1} [partial_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) (ha : a s) :
¬a < hs.min hn
@[simp]
theorem set.is_wf_min_singleton {α : Type u_1} [partial_order α] (a : α) {hs : {a}.is_wf} {hn : {a}.nonempty} :
hs.min hn = a
@[simp]
theorem finset.is_wf_sup {α : Type u_1} {ι : Type u_2} [partial_order α] (f : finset ι) (g : ι → set α) (hf : ∀ (i : ι), i f(g i).is_wf) :
(f.sup g).is_wf
@[simp]
theorem finset.is_pwo_sup {α : Type u_1} {ι : Type u_2} [partial_order α] (f : finset ι) (g : ι → set α) (hf : ∀ (i : ι), i f(g i).is_pwo) :
(f.sup g).is_pwo
theorem set.is_wf.min_le {α : Type u_1} [linear_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) (ha : a s) :
hs.min hn a
theorem set.is_wf.le_min_iff {α : Type u_1} [linear_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) :
a hs.min hn ∀ (b : α), b sa b
theorem set.is_wf.min_le_min_of_subset {α : Type u_1} [linear_order α] {s t : set α} {hs : s.is_wf} {hsn : s.nonempty} {ht : t.is_wf} {htn : t.nonempty} (hst : s t) :
ht.min htn hs.min hsn
theorem set.is_wf.min_union {α : Type u_1} [linear_order α] {s t : set α} (hs : s.is_wf) (hsn : s.nonempty) (ht : t.is_wf) (htn : t.nonempty) :
_.min _ = min (hs.min hsn) (ht.min htn)
theorem set.is_pwo.mul {α : Type u_1} {s t : set α} [ordered_cancel_comm_monoid α] (hs : s.is_pwo) (ht : t.is_pwo) :
(s * t).is_pwo
theorem set.is_pwo.add {α : Type u_1} {s t : set α} [ordered_cancel_add_comm_monoid α] (hs : s.is_pwo) (ht : t.is_pwo) :
(s + t).is_pwo
theorem set.is_wf.add {α : Type u_1} {s t : set α} [linear_ordered_cancel_add_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) :
(s + t).is_wf
theorem set.is_wf.mul {α : Type u_1} {s t : set α} [linear_ordered_cancel_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) :
(s * t).is_wf
theorem set.is_wf.min_add {α : Type u_1} {s t : set α} [linear_ordered_cancel_add_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :
_.min _ = hs.min hsn + ht.min htn
theorem set.is_wf.min_mul {α : Type u_1} {s t : set α} [linear_ordered_cancel_comm_monoid α] (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :
_.min _ = (hs.min hsn) * ht.min htn
def set.partially_well_ordered_on.is_bad_seq {α : Type u_1} (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
theorem set.partially_well_ordered_on.iff_forall_not_is_bad_seq {α : Type u_1} (r : α → α → Prop) (s : set α) :
def set.partially_well_ordered_on.is_min_bad_seq {α : Type u_1} (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
def set.partially_well_ordered_on.min_bad_seq_of_bad_seq {α : Type u_1} (r : α → α → Prop) (rk : α → ) (s : set α) (n : ) (f : → α) (hf : set.partially_well_ordered_on.is_bad_seq r s f) :

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
theorem set.partially_well_ordered_on.exists_min_bad_of_exists_bad {α : Type u_1} (r : α → α → Prop) (rk : α → ) (s : set α) :
theorem set.partially_well_ordered_on.iff_not_exists_is_min_bad_seq {α : Type u_1} {r : α → α → Prop} (rk : α → ) {s : set α} :
theorem set.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂ {α : Type u_1} (r : α → α → Prop) [is_refl α r] [is_trans α r] {s : set α} (h : s.partially_well_ordered_on r) :
{l : list α | ∀ (x : α), x lx s}.partially_well_ordered_on (list.sublist_forall₂ 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.sublist_forall₂ r is partially well-ordered on the set of lists of elements of s. That relation is defined so that list.sublist_forall₂ r l₁ l₂ whenever l₁ related pointwise by r to a sublist of l₂.

theorem set.is_pwo.add_submonoid_closure {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x s0 x) (h : s.is_pwo) :
theorem set.is_pwo.submonoid_closure {α : Type u_1} [ordered_cancel_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x s1 x) (h : s.is_pwo) :
def set.mul_antidiagonal {α : Type u_1} [monoid α] (s t : set α) (a : α) :
set × α)

set.mul_antidiagonal s t a is the set of all pairs of an element in s and an element in t that multiply to a.

Equations
def set.add_antidiagonal {α : Type u_1} [add_monoid α] (s t : set α) (a : α) :
set × α)

set.add_antidiagonal s t a is the set of all pairs of an element in s and an element in t that add to a.

@[simp]
theorem set.add_antidiagonal.mem_add_antidiagonal {α : Type u_1} [add_monoid α] {s t : set α} {a : α} {x : α × α} :
x s.add_antidiagonal t a x.fst + x.snd = a x.fst s x.snd t
@[simp]
theorem set.mul_antidiagonal.mem_mul_antidiagonal {α : Type u_1} [monoid α] {s t : set α} {a : α} {x : α × α} :
x s.mul_antidiagonal t a (x.fst) * x.snd = a x.fst s x.snd t
theorem set.mul_antidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} :
theorem set.add_antidiagonal.fst_eq_fst_iff_snd_eq_snd {α : Type u_1} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.add_antidiagonal t a)} :
theorem set.add_antidiagonal.eq_of_fst_eq_fst {α : Type u_1} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.add_antidiagonal t a)} (h : x.fst = y.fst) :
x = y
theorem set.mul_antidiagonal.eq_of_fst_eq_fst {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} (h : x.fst = y.fst) :
x = y
theorem set.add_antidiagonal.eq_of_snd_eq_snd {α : Type u_1} [add_cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.add_antidiagonal t a)} (h : x.snd = y.snd) :
x = y
theorem set.mul_antidiagonal.eq_of_snd_eq_snd {α : Type u_1} [cancel_comm_monoid α] {s t : set α} {a : α} {x y : (s.mul_antidiagonal t a)} (h : x.snd = y.snd) :
x = y
theorem set.mul_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [ordered_cancel_comm_monoid α] (s t : set α) (a : α) {x y : (s.mul_antidiagonal t a)} (h1 : x.fst y.fst) (h2 : x.snd y.snd) :
x = y
theorem set.add_antidiagonal.eq_of_fst_le_fst_of_snd_le_snd {α : Type u_1} [ordered_cancel_add_comm_monoid α] (s t : set α) (a : α) {x y : (s.add_antidiagonal t a)} (h1 : x.fst y.fst) (h2 : x.snd y.snd) :
x = y
theorem set.mul_antidiagonal.finite_of_is_pwo {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
theorem set.add_antidiagonal.finite_of_is_pwo {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
theorem set.add_antidiagonal.finite_of_is_wf {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :
theorem set.mul_antidiagonal.finite_of_is_wf {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (a : α) :
def finset.mul_antidiagonal {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
finset × α)

finset.mul_antidiagonal_of_is_wf hs ht a is the set of all pairs of an element in s and an element in t that multiply to a, but its construction requires proofs hs and ht that s and t are well-ordered.

Equations
def finset.add_antidiagonal {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) (a : α) :
finset × α)

finset.add_antidiagonal_of_is_wf hs ht a is the set of all pairs of an element in s and an element in t that add to a, but its construction requires proofs hs and ht that s and t are well-ordered.

@[simp]
theorem finset.mem_mul_antidiagonal {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
x finset.mul_antidiagonal hs ht a (x.fst) * x.snd = a x.fst s x.snd t
@[simp]
theorem finset.mem_add_antidiagonal {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {x : α × α} :
theorem finset.mul_antidiagonal_mono_left {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (hus : u s) :
theorem finset.add_antidiagonal_mono_left {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (hus : u s) :
theorem finset.mul_antidiagonal_mono_right {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (hut : u t) :
theorem finset.add_antidiagonal_mono_right {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} {a : α} {u : set α} {hu : u.is_pwo} (hut : u t) :
theorem finset.support_add_antidiagonal_subset_add {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | (finset.add_antidiagonal hs ht a).nonempty} s + t
theorem finset.support_mul_antidiagonal_subset_mul {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
{a : α | (finset.mul_antidiagonal hs ht a).nonempty} s * t
theorem finset.is_pwo_support_add_antidiagonal {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
theorem finset.is_pwo_support_mul_antidiagonal {α : Type u_1} [ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_pwo} {ht : t.is_pwo} :
theorem finset.add_antidiagonal_min_add_min {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :
finset.add_antidiagonal _ _ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
theorem finset.mul_antidiagonal_min_mul_min {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hns : s.nonempty) (hnt : t.nonempty) :
finset.mul_antidiagonal _ _ ((hs.min hns) * ht.min hnt) = {(hs.min hns, ht.min hnt)}
theorem well_founded.is_wf {α : Type u_1} [has_lt α] (h : well_founded has_lt.lt) (s : set α) :