Well-founded sets #

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

Main Definitions #

set.well_founded_on s r indicates that the relation r is well-founded when restricted to the set s.
set.is_wf s indicates that < is well-founded when restricted to s.
set.partially_well_ordered_on s r indicates that the relation r is partially well-ordered (also known as well quasi-ordered) when restricted to the set s.
set.is_pwo s indicates that any infinite sequence of elements in s contains an infinite monotone subsequence. Note that

Definitions for Hahn Series #

set.add_antidiagonal s t a and set.mul_antidiagonal s t a are the sets of pairs of elements from s and t that add/multiply to a.
finset.add_antidiagonal and finset.mul_antidiagonal are finite versions of set.add_antidiagonal and set.mul_antidiagonal defined when s and t are well-founded.

Main Results #

Higman's Lemma, set.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂, shows that if r is partially well-ordered on s, then list.sublist_forall₂ 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.well_founded_on_iff relates well_founded_on to the well-foundedness of a relation on the original type, to avoid dealing with subtypes.
set.is_wf.mono shows that a subset of a well-founded subset is well-founded.
set.is_wf.union shows that the union of two well-founded subsets is well-founded.
finset.is_wf 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 #

source

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

s.well_founded_on r = well_founded (λ (a b : ↥s), r ↑a ↑b)

source

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)

source

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 ∈ s → r z y → P z) → P y) :

P x

source

@[protected, 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)

source

theorem set.well_founded_on_iff_no_descending_seq {α : Type u_1} {s : set α} {r : α → α → Prop} [is_strict_order α r] :

s.well_founded_on r ↔ ∀ (f : gt ↪r r), ¬set.range ⇑f ⊆ s

source

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

s.is_wf = s.well_founded_on has_lt.lt

source

theorem set.is_wf_univ_iff {α : Type u_1} [has_lt α] :

set.univ.is_wf ↔ well_founded has_lt.lt

source

theorem set.is_wf.mono {α : Type u_1} [has_lt α] {s t : set α} (h : t.is_wf) (st : s ⊆ t) :

s.is_wf

source

theorem set.is_wf_iff_no_descending_seq {α : Type u_1} [partial_order α] {s : set α} :

s.is_wf ↔ ∀ (f : order_dual ℕ ↪o α), ¬set.range ⇑f ⊆ s

source

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

source

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

s.partially_well_ordered_on r = ∀ (f : ℕ → α), set.range f ⊆ s → (∃ (m n : ℕ), m < n ∧ r (f m) (f n))

source

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

s.is_pwo = s.partially_well_ordered_on has_le.le

source

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

s.partially_well_ordered_on r

source

theorem set.is_pwo.mono {α : Type u_1} [preorder α] {s t : set α} (ht : t.is_pwo) (hsub : s ⊆ t) :

s.is_pwo

source

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 ∈ s → a2 ∈ s → r a1 a2 → r' (f a1) (f a2)) :

(f '' s).partially_well_ordered_on r'

source

theorem is_antichain.finite_of_partially_well_ordered_on {α : Type u_1} {s : set α} {r : α → α → Prop} (ha : is_antichain r s) (hp : s.partially_well_ordered_on r) :

s.finite

source

theorem set.finite.partially_well_ordered_on {α : Type u_1} {s : set α} {r : α → α → Prop} [is_refl α r] (hs : s.finite) :

s.partially_well_ordered_on r

source

theorem is_antichain.partially_well_ordered_on_iff {α : Type u_1} {s : set α} {r : α → α → Prop} [is_refl α r] (hs : is_antichain r s) :

s.partially_well_ordered_on r ↔ s.finite

source

theorem set.partially_well_ordered_on_iff_finite_antichains {α : Type u_1} {s : set α} {r : α → α → Prop} [is_refl α r] [is_symm α r] :

s.partially_well_ordered_on r ↔ ∀ (t : set α), t ⊆ s → is_antichain r t → t.finite

source

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 ≤ n → r (f (⇑g m)) (f (⇑g n))

source

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 ≤ n → r (f (⇑g m)) (f (⇑g n)))

source

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)

source

theorem set.is_pwo.is_wf {α : Type u_1} {s : set α} [partial_order α] (h : s.is_pwo) :

s.is_wf

source

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)

source

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

source

theorem set.is_pwo.prod {α : Type u_1} {s t : set α} [partial_order α] (hs : s.is_pwo) (ht : t.is_pwo) :

(s ×ˢ t).is_pwo

source

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

source

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

source

theorem set.is_wf.is_pwo {α : Type u_1} [linear_order α] {s : set α} (hs : s.is_wf) :

s.is_pwo

source

theorem set.is_wf_iff_is_pwo {α : Type u_1} [linear_order α] {s : set α} :

s.is_wf ↔ s.is_pwo

source

@[simp]

theorem finset.partially_well_ordered_on {α : Type u_1} {r : α → α → Prop} [is_refl α r] (s : finset α) :

↑s.partially_well_ordered_on r

source

@[simp]

theorem finset.is_pwo {α : Type u_1} [partial_order α] (f : finset α) :

↑f.is_pwo

source

@[simp]

theorem finset.well_founded_on {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : finset α) :

↑f.well_founded_on r

source

@[simp]

theorem finset.is_wf {α : Type u_1} [partial_order α] (f : finset α) :

↑f.is_wf

source

theorem set.finite.is_pwo {α : Type u_1} [partial_order α] {s : set α} (h : s.finite) :

s.is_pwo

source

@[simp]

theorem set.fintype.is_pwo {α : Type u_1} [partial_order α] {s : set α} [fintype α] :

s.is_pwo

source

@[simp]

theorem set.is_pwo_empty {α : Type u_1} [partial_order α] :

∅.is_pwo

source

@[simp]

theorem set.is_pwo_singleton {α : Type u_1} [partial_order α] (a : α) :

{a}.is_pwo

source

theorem set.is_pwo.insert {α : Type u_1} [partial_order α] {s : set α} (a : α) (hs : s.is_pwo) :

(insert a s).is_pwo

source

noncomputable 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

hs.min hn = ↑(well_founded.min hs set.univ _)

source

theorem set.is_wf.min_mem {α : Type u_1} [partial_order α] {s : set α} (hs : s.is_wf) (hn : s.nonempty) :

hs.min hn ∈ s

source

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

source

@[simp]

theorem set.is_wf_min_singleton {α : Type u_1} [partial_order α] (a : α) {hs : {a}.is_wf} {hn : {a}.nonempty} :

hs.min hn = a

source

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

source

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

source

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

source

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 ∈ s → a ≤ b

source

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

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

set.partially_well_ordered_on.is_bad_seq r s f = (set.range f ⊆ s ∧ ∀ (m n : ℕ), m < n → ¬r (f m) (f n))

source

theorem set.partially_well_ordered_on.iff_forall_not_is_bad_seq {α : Type u_1} (r : α → α → Prop) (s : set α) :

s.partially_well_ordered_on r ↔ ∀ (f : ℕ → α), ¬set.partially_well_ordered_on.is_bad_seq r s f

source

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

set.partially_well_ordered_on.is_min_bad_seq r rk s n f = ∀ (g : ℕ → α), (∀ (m : ℕ), m < n → f m = g m) → rk (g n) < rk (f n) → ¬set.partially_well_ordered_on.is_bad_seq r s g

source

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

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

set.partially_well_ordered_on.min_bad_seq_of_bad_seq r rk s n f hf = and.dcases_on _ (λ (h1 : ∀ (m : ℕ), m < n → f m = classical.some _ m) (right : set.partially_well_ordered_on.is_bad_seq r s (classical.some _) ∧ rk (classical.some _ n) = nat.find _), right.dcases_on (λ (h2 : set.partially_well_ordered_on.is_bad_seq r s (classical.some _)) (h3 : rk (classical.some _ n) = nat.find _), ⟨classical.some _, _⟩))

source

theorem set.partially_well_ordered_on.exists_min_bad_of_exists_bad {α : Type u_1} (r : α → α → Prop) (rk : α → ℕ) (s : set α) :

(∃ (f : ℕ → α), set.partially_well_ordered_on.is_bad_seq r s f) → (∃ (f : ℕ → α), set.partially_well_ordered_on.is_bad_seq r s f ∧ ∀ (n : ℕ), set.partially_well_ordered_on.is_min_bad_seq r rk s n f)

source

theorem set.partially_well_ordered_on.iff_not_exists_is_min_bad_seq {α : Type u_1} {r : α → α → Prop} (rk : α → ℕ) {s : set α} :

s.partially_well_ordered_on r ↔ ¬∃ (f : ℕ → α), set.partially_well_ordered_on.is_bad_seq r s f ∧ ∀ (n : ℕ), set.partially_well_ordered_on.is_min_bad_seq r rk s n f

source

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 ∈ l → x ∈ 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₂.

source

theorem set.is_pwo.add_submonoid_closure {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x ∈ s → 0 ≤ x) (h : s.is_pwo) :

↑(add_submonoid.closure s).is_pwo

source

theorem set.is_pwo.submonoid_closure {α : Type u_1} [ordered_cancel_comm_monoid α] {s : set α} (hpos : ∀ (x : α), x ∈ s → 1 ≤ x) (h : s.is_pwo) :

↑(submonoid.closure s).is_pwo

source

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

s.mul_antidiagonal t a = {x : α × α | (x.fst) * x.snd = a ∧ x.fst ∈ s ∧ x.snd ∈ t}

source

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.

Equations

s.add_antidiagonal t a = {x : α × α | x.fst + x.snd = a ∧ x.fst ∈ s ∧ x.snd ∈ t}

source

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

source

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

source

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

↑x.fst = ↑y.fst ↔ ↑x.snd = ↑y.snd

source

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

↑x.fst = ↑y.fst ↔ ↑x.snd = ↑y.snd

source

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

source

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

source

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

source

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

source

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

source

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

source

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

(s.mul_antidiagonal t a).finite

source

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

(s.add_antidiagonal t a).finite

source

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

(s.add_antidiagonal t a).finite

source

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

(s.mul_antidiagonal t a).finite

source

noncomputable 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

finset.mul_antidiagonal hs ht a = _.to_finset

source

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

Equations

finset.add_antidiagonal hs ht a = _.to_finset

source

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

source

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

x ∈ finset.add_antidiagonal hs ht a ↔ x.fst + x.snd = a ∧ x.fst ∈ s ∧ x.snd ∈ t

source

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

finset.mul_antidiagonal hu ht a ⊆ finset.mul_antidiagonal hs ht a

source

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

finset.add_antidiagonal hu ht a ⊆ finset.add_antidiagonal hs ht a

source

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

finset.mul_antidiagonal hs hu a ⊆ finset.mul_antidiagonal hs ht a

source

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

finset.add_antidiagonal hs hu a ⊆ finset.add_antidiagonal hs ht a

source

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

source

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

source

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

{a : α | (finset.add_antidiagonal hs ht a).nonempty}.is_pwo

source

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

{a : α | (finset.mul_antidiagonal hs ht a).nonempty}.is_pwo

source

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

source

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

source

theorem well_founded.is_wf {α : Type u_1} [has_lt α] (h : well_founded has_lt.lt) (s : set α) :

s.is_wf

source

theorem pi.is_pwo {σ : Type u_1} {α : σ → Type u_2} [Π (s : σ), linear_order (α s)] [∀ (s : σ), is_well_order (α s) has_lt.lt] [fintype σ] (S : set (Π (s : σ), α s)) :

S.is_pwo

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 partially_well_ordered_on instead of is_pwo.