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 #

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)
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
@[simp]
theorem finset.is_wf {α : Type u_1} [partial_order α] {f : finset α} :
theorem set.finite.is_wf {α : Type u_1} [partial_order α] {s : set α} (h : s.finite) :
@[simp]
theorem set.fintype.is_wf {α : Type u_1} [partial_order α] {s : set α} [fintype α] :
@[simp]
theorem set.is_wf_empty {α : Type u_1} [partial_order α] :
@[simp]
theorem set.is_wf_singleton {α : Type u_1} [partial_order α] (a : α) :
{a}.is_wf
theorem set.is_wf.insert {α : Type u_1} [partial_order α] {s : set α} (a : α) (hs : s.is_wf) :
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
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)
def set.is_partially_well_ordered {α : 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.is_partially_well_ordered.is_wf {α : Type u_1} [partial_order α] {s : set α} (h : s.is_partially_well_ordered) :
theorem set.is_partially_well_ordered.exists_monotone_subseq {α : Type u_1} [partial_order α] {s : set α} (h : s.is_partially_well_ordered) (f : → α) (hf : set.range f s) :
∃ (g : ↪o ), monotone (f g)
theorem set.is_partially_well_ordered_iff_exists_monotone_subseq {α : Type u_1} [partial_order α] {s : set α} :
s.is_partially_well_ordered ∀ (f : → α), set.range f s(∃ (g : ↪o ), monotone (f g))
theorem set.is_partially_well_ordered.image_of_monotone {α : Type u_1} [partial_order α] {s : set α} {β : Type u_2} [partial_order β] (hs : s.is_partially_well_ordered) {f : α → β} (hf : monotone f) :
theorem set.is_wf.is_partially_well_ordered {α : Type u_1} [linear_order α] {s : set α} (hs : s.is_wf) :
theorem set.is_wf.add {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s + t).is_wf
theorem set.is_wf.mul {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s * t).is_wf
theorem set.is_wf.min_add {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (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} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (hsn : s.nonempty) (htn : t.nonempty) :
_.min _ = (hs.min hsn) * ht.min htn
theorem not_well_founded_swap_of_infinite_of_well_order {α : Type u_1} [infinite α] {r : α → α → Prop} [is_well_order α r] :
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
def set.add_antidiagonal.lt_left {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] (s t : set α) (a : α) (x y : (s.add_antidiagonal t a)) :
Prop

The relation on set.add_antidagonal s t a given by < on the first coordinate.

def set.mul_antidiagonal.lt_left {α : Type u_1} [linear_ordered_cancel_comm_monoid α] (s t : set α) (a : α) (x y : (s.mul_antidiagonal t a)) :
Prop

The relation on set.mul_antidagonal s t a given by < on the first coordinate.

Equations

set.add_antidiagonal s t a ordered by lt_left embeds into s

set.mul_antidiagonal s t a ordered by lt_left embeds into s

Equations

set.mul_antidiagonal s t a ordered by lt_left embeds into the dual of t

Equations

set.add_antidiagonal s t a ordered by lt_left embeds into the dual of t

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} [linear_ordered_cancel_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (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} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) (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} [linear_ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {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} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {a : α} {x : α × α} :
theorem finset.mul_antidiagonal_mono_left {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {a : α} {u : set α} {hu : u.is_wf} (hus : u s) :
theorem finset.add_antidiagonal_mono_left {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {a : α} {u : set α} {hu : u.is_wf} (hus : u s) :
theorem finset.mul_antidiagonal_mono_right {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {a : α} {u : set α} {hu : u.is_wf} (hut : u t) :
theorem finset.add_antidiagonal_mono_right {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} {a : α} {u : set α} {hu : u.is_wf} (hut : u t) :
theorem finset.support_add_antidiagonal_subset_add {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} :
{a : α | (finset.add_antidiagonal hs ht a).nonempty} s + t
theorem finset.support_mul_antidiagonal_subset_mul {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} :
{a : α | (finset.mul_antidiagonal hs ht a).nonempty} s * t
theorem finset.is_wf_support_add_antidiagonal {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} :
theorem finset.is_wf_support_mul_antidiagonal {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s t : set α} {hs : s.is_wf} {ht : t.is_wf} :
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 ht (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 ht ((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 α) :