Set.IsPWO.union
theorem Set.IsPWO.union : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, s.IsPWO → t.IsPWO → (s ∪ t).IsPWO := by
sorry
This theorem states that for any type `α` with a preorder structure, if two sets `s` and `t` are partially well-ordered — that is, any infinite sequence in these sets contain a monotone subsequence of length 2 — then the union of `s` and `t` is also partially well-ordered.
More concisely: If `α` is a type with a preorder structure and `s` and `t` are partially well-ordered sets, then the union of `s` and `t` is also partially well-ordered.
|
Set.IsWF.not_lt_min
theorem Set.IsWF.not_lt_min :
∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty), a ∈ s → ¬a < hs.min hn
This theorem states that, for any given type `α` that has a preorder relation and any set `s` of type `α` that is well-founded and nonempty, for any element `a` that belongs to this set `s`, there cannot be an element `a` that is less than the minimum element of the set `s`. In other words, there's no element in a nonempty well-founded set that is less than the minimum element of that set.
More concisely: In a nonempty, well-founded set endowed with a preorder relation, there is no element less than the minimum element.
|
Set.IsWF.min_le
theorem Set.IsWF.min_le :
∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty),
a ∈ s → hs.min hn ≤ a
The theorem `Set.IsWF.min_le` asserts that for any type `α` with a linear order, given any well-founded set `s` of the type `α` which is nonempty, for any element `a` in the set `s`, the minimal element of the set `s`, as determined by the `Set.IsWF.min` function, is less than or equal to `a`. In other words, it confirms that the `Set.IsWF.min` function indeed returns a minimum element of the well-founded set.
More concisely: For any nonempty well-founded set `s` of a type `α` with a linear order, the minimal element of `s` is less than or equal to every element `a` in `s`.
|
Pi.isPWO
theorem Pi.isPWO :
∀ {ι : Type u_1} {α : ι → Type u_6} [inst : (i : ι) → LinearOrder (α i)]
[inst_1 : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1] [inst_2 : Finite ι] (s : Set ((i : ι) → α i)),
s.IsPWO
The theorem `Pi.isPWO` is a version of Dickson's lemma. The theorem states that for any subset of functions `Π s : σ, α s`, it is partially well-ordered. This condition holds when `σ` is a finite type (`Fintype`) and each `α s` is a well-ordered linear order. This includes the classical case of Dickson's lemma that states `ℕ ^ n` (the set of n-tuples of natural numbers) is a well partial order. The proof of this theorem could potentially be generalized to include cases where the target is only partially well ordered, or to consider the case where we use `Set.PartiallyWellOrderedOn` instead of `Set.IsPWO`.
More concisely: For any type `σ` and family of sets `Π s : σ, α s` where each `α s` is a well-ordered linear order, the product `Π s, α s` is a partially well-ordered set.
|
Set.IsWF.isPWO
theorem Set.IsWF.isPWO : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α}, s.IsWF → s.IsPWO
This theorem states that for any type `α` equipped with a linear order, and for any set `s` of this type, if `s` is well-founded with respect to the `<` relation, then it is also partially well-ordered. In other words, if every non-empty subset of `s` has a least element, then any infinite sequence from `s` contains a monotone subsequence of length 2 or equivalently, an infinite monotone subsequence, where monotonicity is defined with respect to the `≤` relation.
More concisely: If `α` is a type with a linear order and `s` is a well-founded subset of `α`, then `s` has an infinite monotone subsequence.
|
Set.IsWF.min_mem
theorem Set.IsWF.min_mem :
∀ {α : Type u_2} [inst : Preorder α] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty), hs.min hn ∈ s
This theorem states that, for any type `α` with a preorder relation, and for any set `s` of type `α`, if `s` is well-founded with respect to the `<` relation (that is, there are no infinitely decreasing sequences) and `s` is nonempty, then the minimum element of `s` (obtained via the `Set.IsWF.min` function) is indeed an element of `s`. In other words, the function `Set.IsWF.min` is guaranteed to return an element that belongs to the set `s`, provided `s` is both well-founded and nonempty.
More concisely: If `s` is a nonempty, well-founded set with respect to a preorder relation in Lean, then `Set.IsWF.min s` is an element of `s`.
|
Set.isWF_iff_isPWO
theorem Set.isWF_iff_isPWO : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α}, s.IsWF ↔ s.IsPWO
This theorem states that in the context of a linear order, the properties of being well-founded (`Set.IsWF`) and being a partially well-ordered set (`Set.IsPWO`) are equivalent for a given set. A set is said to be well-founded if there is no infinite descending sequence of elements in it, and a set is said to be partially well-ordered if any infinite sequence from it contains an infinite monotonically increasing subsequence. Therefore, this theorem provides an equivalence between these two properties in the case of linearly ordered sets.
More concisely: In a linearly ordered set, a set is well-founded if and only if it is partially well-ordered.
|
Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂
theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ :
∀ {α : Type u_2} (r : α → α → Prop) [inst : IsRefl α r] [inst : IsTrans α r] {s : Set α},
s.PartiallyWellOrderedOn r → {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)
This theorem is a statement of Higman's Lemma in the language of Lean. It states that if we have a reflexive and transitive relation `r` that is partially well-ordered on a set `s`, then the relation `List.SublistForall₂ r` is also partially well-ordered on the set of lists of elements of `s`. Here, `List.SublistForall₂ r` is a relation defined such that `List.SublistForall₂ r l₁ l₂` holds whenever each element in the list `l₁` is related to some element in a sublist of `l₂` by the relation `r`. In other words, if a certain order can be applied to the elements of a set, then the same kind of order can be applied to lists of those elements.
More concisely: If `r` is a reflexive, transitive, and partially well-ordered relation on a set `s`, then the relation `List.SublistForall₂ r` is also partially well-ordered on the set of lists of elements from `s`.
|
Set.PartiallyWellOrderedOn.image_of_monotone_on
theorem Set.PartiallyWellOrderedOn.image_of_monotone_on :
∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {f : α → β} {s : Set α},
s.PartiallyWellOrderedOn r →
(∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) → (f '' s).PartiallyWellOrderedOn r'
The theorem `Set.PartiallyWellOrderedOn.image_of_monotone_on` establishes a property of sets that are partially well-ordered by a binary relation. Specifically, for any types `α` and `β`, any relations `r` on `α` and `r'` on `β`, a function `f` from `α` to `β`, and a set `s` of type `α`, if the set `s` is partially well-ordered by `r`, and for any two elements `a₁` and `a₂` in `s` such that `a₁` is related to `a₂` by `r`, `f(a₁)` is related to `f(a₂)` by `r'`, then the image of `s` under `f` is partially well-ordered by `r'`. In other words, this theorem asserts that the partial well-ordering property is preserved under the image of a monotone function.
More concisely: If `s` is a partially well-ordered set under relation `r`, and `f : α → β` is a monotone function (i.e., `a r b` implies `f a r' f b` for all `a, b` in `α` and relation `r'` on `β`), then the image `{f x | x ∈ s}` is a partially well-ordered set under relation `r'`.
|
Set.PartiallyWellOrderedOn.exists_monotone_subseq
theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq :
∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [inst : IsRefl α r] [inst : IsTrans α r],
s.PartiallyWellOrderedOn r →
∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
This theorem states that for any type `α`, relation `r`, and set `s`, if `r` is a reflexive and transitive relation on `α`, and if `s` is partially well-ordered by `r`, then for any sequence `f` from natural numbers to `α` where all elements of the sequence belong to `s`, there exists a subsequence `g` such that for all natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the `m`-th element of the subsequence `g` is related to the `n`-th element of `g` via the relation `r`.
In other words, it guarantees the existence of a monotone subsequence for any sequence that only contains elements from a set that is partially well-ordered by a reflexive and transitive relation.
More concisely: Given a type `α`, a reflexive and transitive relation `r` on `α`, and a partially well-ordered set `s` (under `r`), any strictly increasing sequence of natural numbers `n` indexing elements in `s` has a monotone subsequence `g` such that `r(g(m), g(n))` holds for all `m ≤ n`.
|
Set.IsWF.le_min_iff
theorem Set.IsWF.le_min_iff :
∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty),
a ≤ hs.min hn ↔ ∀ b ∈ s, a ≤ b
This theorem states that for any set `s` of a given type `α`, where `α` is endowed with a linear order and `s` is both well-founded and non-empty, an element `a` of type `α` is less than or equal to the minimal element of `s` if and only if `a` is less than or equal to every element of `s`. In other words, if `s` is a set of elements with a certain order, and it's nonempty and well-founded (i.e., there is no infinite decreasing sequence of elements in `s`), then `a` being less than or equal to the smallest element in `s` is equivalent to `a` being less than or equal to all elements in `s`. This is a characterization of the minimum element in a well-founded and non-empty set with a linear order.
More concisely: For any well-founded and non-empty set `s` with a linear order, an element `a` is the minimal element if and only if `a` is less than or equal to every element in `s`.
|
Set.Finite.partiallyWellOrderedOn
theorem Set.Finite.partiallyWellOrderedOn :
∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [inst : IsRefl α r], s.Finite → s.PartiallyWellOrderedOn r := by
sorry
The theorem `Set.Finite.partiallyWellOrderedOn` states that for any given type `α`, relation `r` on `α`, and set `s` of type `α`, where `r` is a reflexive relation (meaning that every element is related to itself), if the set `s` is finite, then `s` is partially well-ordered by the relation `r`. In other words, for any infinite sequence drawn from the set `s`, there exist two indices `m` and `n` such that `m` is less than `n` and the `m`-th element of the sequence is related to the `n`-th element via `r`.
More concisely: If `α` is a type, `r` is a reflexive relation on `α`, and `s` is a finite set of `α` with respect to `=`, then `s` is partially ordered by `r`.
|
Mathlib.Order.WellFoundedSet._auxLemma.20
theorem Mathlib.Order.WellFoundedSet._auxLemma.20 : ∀ (p : Prop), (True ∧ p) = p
This theorem, termed as `Mathlib.Order.WellFoundedSet._auxLemma.20`, states that for any proposition `p`, the logical conjunction of `True` and `p` is equivalent to `p` itself. In other words, if `p` is a proposition, then `True and p` is just `p`, because the truth-value of the conjunction is solely determined by `p` when the other conjunct is `True`.
More concisely: For any proposition `p`, `True` and `p` are logically equivalent.
|
Set.Finite.isPWO
theorem Set.Finite.isPWO : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Finite → s.IsPWO
The theorem `Set.Finite.isPWO` states that for any type `α` with a preorder relation, and any set `s` of that type, if the set `s` is finite, then it is partially well-ordered. In other words, if we have a finite set from a preordered type, then any infinite sequence from that set contains a monotone subsequence of length 2 or equivalently, an infinite monotone subsequence.
More concisely: If `α` is a type with a preorder relation and `s : α` is a finite set, then `s` is partially well-ordered, i.e., it has an infinite monotone subsequence.
|
WellFounded.sigma_lex_of_wellFoundedOn_fiber
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},
WellFounded (rι on f) →
(∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)) →
WellFounded (Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩)
This theorem, `WellFounded.sigma_lex_of_wellFoundedOn_fiber`, establishes that for any types `ι`, `γ`, `π`, any relations `rι` and `rπ`, and any functions `f` and `g`, if the relation `rι on f` is well-founded and the relation `rπ i on g i` is well-founded on the preimage of `{i}` under `f` for all `i`, then the relation `Sigma.Lex rι rπ on fun c => ⟨f c, g (f c) c⟩` is also well-founded. Here, `Sigma.Lex rι rπ` represents a lexicographic order on the Sigma types generated by `ι` and `π` defined by the relations `rι` and `rπ`.
More concisely: If relations `rι` on `f` and `rπ` on `g(fc)` are well-founded for all `i` in a type `ι`, then the lexicographic relation `Sigma.Lex rι rπ` on pairs `⟨fc, ci⟩` where `fc = f(ci)`, is also well-founded.
|
Set.IsPWO.isWF
theorem Set.IsPWO.isWF : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO → s.IsWF
The theorem `Set.IsPWO.isWF` states that for any type `α` equipped with a preorder and any set `s` of type `α`, if `s` is partially well-ordered (meaning that any infinite sequence in `s` contains a monotone subsequence of length 2, or equivalently, an infinite monotone subsequence), then `s` is also well-founded with respect to the `<` operation. In other words, if `s` is partially well-ordered, then every non-empty subset of `s` has a minimal element under the `<` operation.
More concisely: If a preordered set is partially well-ordered, then it is well-founded.
|
Set.IsPWO.image_of_monotone
theorem Set.IsPWO.image_of_monotone :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
s.IsPWO → ∀ {f : α → β}, Monotone f → (f '' s).IsPWO
The theorem `Set.IsPWO.image_of_monotone` states that for any types `α` and `β` with preorders, any subset `s` of `α` that is partially well-ordered, and any monotone function `f` from `α` to `β`, the image of `s` under `f` (denoted as `f '' s`) is also partially well-ordered. In other words, if a set is partially well-ordered and a function is monotone, then the set obtained by applying the function to every element of the original set is also partially well-ordered.
More concisely: If `α` is a type with a preorder, `s ⊆ α` is partially well-ordered, and `f : α → β` is a monotone function, then `f '' s ⊆ β` is partially well-ordered.
|
Set.WellFoundedOn.acc_iff_wellFoundedOn
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
The theorem states that for any type `α` and any relation `r` on elements of `α`, an element `a` of type `α` is said to be accessible under the relation `r` if and only if the relation `r` is well-founded on the downward transitive closure of `a` under `r`. Here, the downward transitive closure can either include `a` or not. In other words, this theorem provides a characterization of accessibility in terms of well-foundedness of a relation on the downward transitive closure of an element.
More concisely: An element is accessible under a relation if and only if the relation is well-founded on its downward transitive closure, which may or may not include the element.
|
Set.WellFoundedOn.subset
theorem Set.WellFoundedOn.subset :
∀ {α : Type u_2} {r : α → α → Prop} {s t : Set α}, t.WellFoundedOn r → s ⊆ t → s.WellFoundedOn r
This theorem states that for any type `α`, any relation `r` on `α`, and any two sets `s` and `t` of type `α`, if the relation `r` is well-founded on set `t` and set `s` is a subset of `t`, then the relation `r` is also well-founded on set `s`. Here, a relation `r` is said to be well-founded on a set if every non-empty subset has a minimal element under the relation.
More concisely: If relation `r` is well-founded on set `t` and `s` is a subset of `t`, then `r` is well-founded on `s`.
|
Set.IsPWO.mono
theorem Set.IsPWO.mono : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, t.IsPWO → s ⊆ t → s.IsPWO
The theorem `Set.IsPWO.mono` states that for all types `α` equipped with a preorder, if we have two sets `s` and `t` of this type such that `t` is partially well-ordered and `s` is a subset of `t`, then `s` is also partially well-ordered. In other words, the property of being partially well-ordered is preserved under taking subsets. In this context, a set is partially well-ordered if any infinite sequence from the set contains a monotone subsequence of length 2 or, equivalently, an infinite monotone subsequence.
More concisely: If `α` is a type with a preorder, and `s` is a subset of the partially well-ordered set `t`, then `s` is also partially well-ordered.
|
Set.IsWF.min_le_min_of_subset
theorem Set.IsWF.min_le_min_of_subset :
∀ {α : Type u_2} [inst : LinearOrder α] {s t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF}
{htn : t.Nonempty}, s ⊆ t → ht.min htn ≤ hs.min hsn
This theorem, `Set.IsWF.min_le_min_of_subset`, states that for any two sets `s` and `t` of a type `α` which is equipped with a linear order, if both sets are well-founded (meaning the less-than operation is well-founded when restricted to these sets) and nonempty, then if `s` is a subset of `t`, the minimum element of `t` is less than or equal to the minimum element of `s`. In this context, the minimum element of a well-founded, nonempty set is defined with respect to the given order on `α`.
More concisely: If `s` is a nonempty, well-founded subset of a well-founded, nonempty set `t` with respect to a linear order on their common type `α`, then the minimum element of `s` is less than or equal to the minimum element of `t`.
|
WellFounded.prod_lex_of_wellFoundedOn_fiber
theorem WellFounded.prod_lex_of_wellFoundedOn_fiber :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β},
WellFounded (rα on f) →
(∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)) → WellFounded (Prod.Lex rα rβ on fun c => (f c, g c))
This theorem, `WellFounded.prod_lex_of_wellFoundedOn_fiber`, asserts that for any types `α`, `β`, and `γ`, and for any relations `rα` on `α`, `rβ` on `β`, and functions `f` mapping `γ` to `α` and `g` mapping `γ` to `β`, if the relation `rα` is well-founded on the function `f` and the relation `rβ` is well-founded on the preimage of each element `a` of `α` under `f`, then the lexicographic product of the relations `rα` and `rβ` is well-founded on the pair of functions `(f, g)`.
In simpler terms, this theorem states that a lexicographic ordering, formed from two well-founded orderings, remains well-founded when applied to pairs of elements produced by two functions, provided that one of the orderings is well-founded on each "fiber" (preimage) of the first function.
More concisely: If relations `rα` on `α` and `rβ` on `β` are well-founded on `f: γ → α` and `g: γ → β`, respectively, then their lexicographic product is well-founded on `(f, g): γ → α × β`.
|
Set.Finite.isWF
theorem Set.Finite.isWF : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Finite → s.IsWF
This theorem states that for any type `α` with a Preorder structure, if a set `s` of type `α` is finite, then the relation `<` is well-founded when restricted to this set `s`. In other words, for every set of elements of a type which has a preorder (a relation that is reflexive and transitive), if the set is finite, there are no infinite descending `<` chains in the set.
More concisely: For any finite subset of a preordered type, the preorder relation is well-founded.
|