scilib documentation

def set.well_founded_on {α : Type u_2} (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)

@[simp]

theorem set.well_founded_on_empty {α : Type u_2} (r : α → α → Prop) :

∅.well_founded_on r

theorem set.well_founded_on_iff {α : Type u_2} {r : α → α → Prop} {s : set α} :

s.well_founded_on r ↔ well_founded (λ (a b : α), r a b ∧ a ∈ s ∧ b ∈ s)

@[protected]

theorem set.well_founded_on.induction {α : Type u_2} {r : α → α → Prop} {s : set α} {x : α} (hs : s.well_founded_on r) (hx : x ∈ s) {P : α → Prop} (hP : ∀ (y : α), y ∈ s → (∀ (z : α), z ∈ s → r z y → P z) → P y) :

P x

@[protected]

theorem set.well_founded_on.mono {α : Type u_2} {r r' : α → α → Prop} {s t : set α} (h : t.well_founded_on r') (hle : r ≤ r') (hst : s ⊆ t) :

theorem set.well_founded_on.subset {α : Type u_2} {r : α → α → Prop} {s t : set α} (h : t.well_founded_on r) (hst : s ⊆ t) :

theorem set.well_founded_on.acc_iff_well_founded_on {α : Type u_1} {r : α → α → Prop} {a : α} :

[acc r a, {b : α | relation.refl_trans_gen r b a}.well_founded_on r, {b : α | relation.trans_gen r b a}.well_founded_on 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).

@[protected, instance]

def set.is_strict_order.subset {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s : set α} :

is_strict_order α (λ (a b : α), r a b ∧ a ∈ s ∧ b ∈ s)

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

s.well_founded_on r ↔ ∀ (f : gt ↪r r), ¬∀ (n : ℕ), ⇑f n ∈ s

theorem set.well_founded_on.union {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s t : set α} (hs : s.well_founded_on r) (ht : t.well_founded_on r) :

(s ∪ t).well_founded_on r

@[simp]

theorem set.well_founded_on_union {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s t : set α} :

(s ∪ t).well_founded_on r ↔ s.well_founded_on r ∧ t.well_founded_on r

Sets well-founded w.r.t. the strict inequality #

def set.is_wf {α : Type u_2} [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

@[simp]

theorem set.is_wf_empty {α : Type u_2} [has_lt α] :

∅.is_wf

set.univ.is_wf ↔ well_founded has_lt.lt

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

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

@[protected]

theorem set.is_wf.union {α : Type u_2} [preorder α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :

(s ∪ t).is_wf

@[simp]

theorem set.is_wf_union {α : Type u_2} [preorder α] {s t : set α} :

(s ∪ t).is_wf ↔ s.is_wf ∧ t.is_wf

theorem set.is_wf_iff_no_descending_seq {α : Type u_2} [preorder α] {s : set α} :

s.is_wf ↔ ∀ (f : ℕ → α), strict_anti f → (¬∀ (n : ℕ), f (⇑order_dual.to_dual n) ∈ s)

Partially well-ordered sets #

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 is_antichain) is finite, see set.partially_well_ordered_on_iff_finite_antichains.

def set.partially_well_ordered_on {α : Type u_2} (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 : ℕ → α), (∀ (n : ℕ), f n ∈ s) → (∃ (m n : ℕ), m < n ∧ r (f m) (f n))

theorem set.partially_well_ordered_on.mono {α : Type u_2} {r : α → α → Prop} {s t : set α} (ht : t.partially_well_ordered_on r) (h : s ⊆ t) :

s.partially_well_ordered_on r

∅.partially_well_ordered_on r

@[simp]

theorem set.partially_well_ordered_on_empty {α : Type u_2} (r : α → α → Prop) :

theorem set.partially_well_ordered_on.union {α : Type u_2} {r : α → α → Prop} {s t : set α} (hs : s.partially_well_ordered_on r) (ht : t.partially_well_ordered_on r) :

(s ∪ t).partially_well_ordered_on r

@[simp]

theorem set.partially_well_ordered_on_union {α : Type u_2} {r : α → α → Prop} {s t : set α} :

(s ∪ t).partially_well_ordered_on r ↔ s.partially_well_ordered_on r ∧ t.partially_well_ordered_on r

theorem set.partially_well_ordered_on.image_of_monotone_on {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {f : α → β} {s : set α} (hs : s.partially_well_ordered_on r) (hf : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → r a₁ a₂ → r' (f a₁) (f a₂)) :

(f '' s).partially_well_ordered_on r'

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

s.finite

@[protected]

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

s.partially_well_ordered_on r

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

s.partially_well_ordered_on r ↔ s.finite

@[simp]

theorem set.partially_well_ordered_on_singleton {α : Type u_2} {r : α → α → Prop} [is_refl α r] (a : α) :

{a}.partially_well_ordered_on r

@[simp]

theorem set.partially_well_ordered_on_insert {α : Type u_2} {r : α → α → Prop} {s : set α} {a : α} [is_refl α r] :

(has_insert.insert a s).partially_well_ordered_on r ↔ s.partially_well_ordered_on r

@[protected]

theorem set.partially_well_ordered_on.insert {α : Type u_2} {r : α → α → Prop} {s : set α} [is_refl α r] (h : s.partially_well_ordered_on r) (a : α) :

(has_insert.insert a s).partially_well_ordered_on r

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

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

theorem set.partially_well_ordered_on.exists_monotone_subseq {α : Type u_2} {r : α → α → Prop} {s : set α} [is_refl α r] [is_trans α r] (h : s.partially_well_ordered_on r) (f : ℕ → α) (hf : ∀ (n : ℕ), f n ∈ s) :

∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (⇑g m)) (f (⇑g n))

theorem set.partially_well_ordered_on_iff_exists_monotone_subseq {α : Type u_2} {r : α → α → Prop} {s : set α} [is_refl α r] [is_trans α r] :

s.partially_well_ordered_on r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → (∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f (⇑g m)) (f (⇑g n)))

@[protected]

theorem set.partially_well_ordered_on.prod {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {s : set α} [is_refl α r] [is_trans α r] {t : set β} (hs : s.partially_well_ordered_on r) (ht : t.partially_well_ordered_on r') :

(s ×ˢ t).partially_well_ordered_on (λ (x y : α × β), r x.fst y.fst ∧ r' x.snd y.snd)

theorem set.partially_well_ordered_on.well_founded_on {α : Type u_2} {r : α → α → Prop} {s : set α} [is_preorder α r] (h : s.partially_well_ordered_on r) :

s.well_founded_on (λ (a b : α), r a b ∧ ¬r b a)

def set.is_pwo {α : Type u_2} [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

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

s ⊆ t → s.is_pwo

theorem set.is_pwo.exists_monotone_subseq {α : Type u_2} [preorder α] {s : set α} (h : s.is_pwo) (f : ℕ → α) (hf : ∀ (n : ℕ), f n ∈ s) :

∃ (g : ℕ ↪o ℕ), monotone (f ∘ ⇑g)

theorem set.is_pwo_iff_exists_monotone_subseq {α : Type u_2} [preorder α] {s : set α} :

s.is_pwo ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → (∃ (g : ℕ ↪o ℕ), monotone (f ∘ ⇑g))

@[protected]

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

theorem set.is_pwo.prod {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} {t : set β} (hs : s.is_pwo) (ht : t.is_pwo) :

(s ×ˢ t).is_pwo

theorem set.is_pwo.image_of_monotone_on {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} (hs : s.is_pwo) {f : α → β} (hf : monotone_on f s) :

(f '' s).is_pwo

theorem set.is_pwo.image_of_monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} (hs : s.is_pwo) {f : α → β} (hf : monotone f) :

(f '' s).is_pwo

@[protected]

theorem set.is_pwo.union {α : Type u_2} [preorder α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) :

(s ∪ t).is_pwo

@[simp]

theorem set.is_pwo_union {α : Type u_2} [preorder α] {s t : set α} :

(s ∪ t).is_pwo ↔ s.is_pwo ∧ t.is_pwo

@[protected]

theorem set.finite.is_pwo {α : Type u_2} [preorder α] {s : set α} (hs : s.finite) :

@[simp]

theorem set.is_pwo_of_finite {α : Type u_2} [preorder α] {s : set α} [finite α] :

@[simp]

theorem set.is_pwo_singleton {α : Type u_2} [preorder α] (a : α) :

{a}.is_pwo

@[simp]

theorem set.is_pwo_empty {α : Type u_2} [preorder α] :

∅.is_pwo

@[protected]

theorem set.subsingleton.is_pwo {α : Type u_2} [preorder α] {s : set α} (hs : s.subsingleton) :

@[simp]

theorem set.is_pwo_insert {α : Type u_2} [preorder α] {s : set α} {a : α} :

(has_insert.insert a s).is_pwo ↔ s.is_pwo

@[protected]

theorem set.is_pwo.insert {α : Type u_2} [preorder α] {s : set α} (h : s.is_pwo) (a : α) :

(has_insert.insert a s).is_pwo

@[protected]

theorem set.finite.is_wf {α : Type u_2} [preorder α] {s : set α} (hs : s.finite) :

@[simp]

theorem set.is_wf_singleton {α : Type u_2} [preorder α] {a : α} :

{a}.is_wf

@[protected]

theorem set.subsingleton.is_wf {α : Type u_2} [preorder α] {s : set α} (hs : s.subsingleton) :

@[simp]

theorem set.is_wf_insert {α : Type u_2} [preorder α] {s : set α} {a : α} :

(has_insert.insert a s).is_wf ↔ s.is_wf

theorem set.is_wf.insert {α : Type u_2} [preorder α] {s : set α} (h : s.is_wf) (a : α) :

(has_insert.insert a s).is_wf

@[protected]

theorem set.finite.well_founded_on {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s : set α} (hs : s.finite) :

@[simp]

theorem set.well_founded_on_singleton {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {a : α} :

{a}.well_founded_on r

@[protected]

theorem set.subsingleton.well_founded_on {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s : set α} (hs : s.subsingleton) :

@[simp]

theorem set.well_founded_on_insert {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s : set α} {a : α} :

(has_insert.insert a s).well_founded_on r ↔ s.well_founded_on r

theorem set.well_founded_on.insert {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] {s : set α} (h : s.well_founded_on r) (a : α) :

(has_insert.insert a s).well_founded_on r

@[protected]

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

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

s.is_wf ↔ s.is_pwo

In a linear order, the predicates set.is_wf and set.is_pwo are equivalent.

@[protected, simp]

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

↑s.partially_well_ordered_on r

@[protected, simp]

theorem finset.is_pwo {α : Type u_2} [preorder α] (s : finset α) :

↑s.is_pwo

@[protected, simp]

theorem finset.is_wf {α : Type u_2} [preorder α] (s : finset α) :

↑s.is_wf

@[protected, simp]

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

↑s.well_founded_on r

theorem finset.well_founded_on_sup {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] (s : finset ι) {f : ι → set α} :

(s.sup f).well_founded_on r ↔ ∀ (i : ι), i ∈ s → (f i).well_founded_on r

theorem finset.partially_well_ordered_on_sup {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : finset ι) {f : ι → set α} :

(s.sup f).partially_well_ordered_on r ↔ ∀ (i : ι), i ∈ s → (f i).partially_well_ordered_on r

theorem finset.is_wf_sup {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι → set α} :

(s.sup f).is_wf ↔ ∀ (i : ι), i ∈ s → (f i).is_wf

theorem finset.is_pwo_sup {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι → set α} :

(s.sup f).is_pwo ↔ ∀ (i : ι), i ∈ s → (f i).is_pwo

@[simp]

theorem finset.well_founded_on_bUnion {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} [is_strict_order α r] (s : finset ι) {f : ι → set α} :

(⋃ (i : ι) (H : i ∈ s), f i).well_founded_on r ↔ ∀ (i : ι), i ∈ s → (f i).well_founded_on r

@[simp]

theorem finset.partially_well_ordered_on_bUnion {ι : Type u_1} {α : Type u_2} {r : α → α → Prop} (s : finset ι) {f : ι → set α} :

(⋃ (i : ι) (H : i ∈ s), f i).partially_well_ordered_on r ↔ ∀ (i : ι), i ∈ s → (f i).partially_well_ordered_on r

@[simp]

theorem finset.is_wf_bUnion {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι → set α} :

(⋃ (i : ι) (H : i ∈ s), f i).is_wf ↔ ∀ (i : ι), i ∈ s → (f i).is_wf

@[simp]

theorem finset.is_pwo_bUnion {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι → set α} :

(⋃ (i : ι) (H : i ∈ s), f i).is_pwo ↔ ∀ (i : ι), i ∈ s → (f i).is_pwo

noncomputable def set.is_wf.min {α : Type u_2} [preorder α] {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 _)

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

hs.min hn ∈ s

theorem set.is_wf.not_lt_min {α : Type u_2} [preorder α] {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_2} [preorder α] (a : α) {hs : {a}.is_wf} {hn : {a}.nonempty} :

hs.min hn = a

theorem set.is_wf.min_le {α : Type u_2} [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_2} [linear_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) :

a ≤ hs.min hn ↔ ∀ (b : α), b ∈ s → a ≤ b

theorem set.is_wf.min_le_min_of_subset {α : Type u_2} [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_2} [linear_order α] {s t : set α} (hs : s.is_wf) (hsn : s.nonempty) (ht : t.is_wf) (htn : t.nonempty) :

_.min _ = linear_order.min (hs.min hsn) (ht.min htn)

def set.partially_well_ordered_on.is_bad_seq {α : Type u_2} (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 = ((∀ (n : ℕ), f n ∈ s) ∧ ∀ (m n : ℕ), m < n → ¬r (f m) (f n))

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

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

def set.partially_well_ordered_on.is_min_bad_seq {α : Type u_2} (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

noncomputable def set.partially_well_ordered_on.min_bad_seq_of_bad_seq {α : Type u_2} (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 _, _⟩))

theorem set.partially_well_ordered_on.exists_min_bad_of_exists_bad {α : Type u_2} (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)

theorem set.partially_well_ordered_on.iff_not_exists_is_min_bad_seq {α : Type u_2} {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

theorem set.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂ {α : Type u_2} (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₂.

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

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